X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=86675e553e48abf02c18c78ecf1043341445b65f;hb=c1dfb763206c3e548b26d1e5f2128c6938a5df14;hp=e130b4fb6aff8fceeaf5436ebcf3cb8410a61066;hpb=8e1a7e55cbc7750446f0a7ab3d071190594243fb;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index e130b4fb6..86675e553 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -319,6 +319,23 @@
+
+
+
+
+ AS
+
+
+
+
+
+
+ __
+
+
+
+
+
@@ -366,6 +383,7 @@
+
@@ -379,7 +397,7 @@
-
+
@@ -394,7 +412,7 @@
-
+
:
@@ -403,13 +421,56 @@
+
+
+
+
+
+
+ LET
+ _
+
+
+
+
+
+
+ =
+
+
+
+
+
+
+
+ IN
+ _
+
+
+
+
+
+
+
+ LET
+ _
+
+ =
+
+ _
+ IN
+ _
+
+
+
+
- Π
+ Π
@@ -424,7 +485,7 @@
- Π
+ Π
:
@@ -440,7 +501,9 @@
- (
+
+ (
+
@@ -448,11 +511,27 @@
- →
-
+ →
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -460,14 +539,34 @@
+
- (
+
+ (
+
- →
-
- )
+ →
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ )
+
@@ -528,7 +627,7 @@
- :>
+ :>
@@ -545,7 +644,7 @@
(
- :>
+ :>
)
@@ -614,7 +713,7 @@
_
- ⇒
+ ⇒
@@ -625,7 +724,7 @@
|_
- ⇒
+ ⇒
@@ -655,7 +754,7 @@
- ⇒
+ ⇒
_
@@ -856,7 +955,7 @@
- we proved
+ we proved
_
@@ -864,6 +963,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -891,55 +1008,111 @@
)
-
+
-
-
+
+
- Consider
-
+ Consider
+ _
+
-
-
-
-
-
Rewrite
_
-
+
_
with
_
-
+
_
by
_
-
- _
- in
- _
-
- _
- and apply to
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Consider
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Then apply it to
_
-
+
-
+
+
+
+
+
+
+ By induction
+
+
+
+
+
+ base case:
+
+
+
+
+
+
+
+ inductive case:
+
+
+
+
+
+
+
@@ -950,7 +1123,8 @@
- Consider
+ Consider
+ _
@@ -1038,6 +1212,50 @@
+
+
+
+
+
+
+
+
+
+
+ Consider
+ _
+
+
+
+
+
+
+
+
+ Let
+ _
+
+ :
+
+ _
+ such that
+ _
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1045,6 +1263,7 @@
+
@@ -1109,7 +1328,7 @@
- λ
+ λ
@@ -1124,7 +1343,7 @@
- λ
+ λ
:
@@ -1163,9 +1382,7 @@
__
-
- =
-
+ =
@@ -1429,7 +1646,7 @@
- >
+
@@ -1441,3 +1658,5 @@
+
+