X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6e66736a32aeb8e1fc866033a8091fc511f028f7;hb=2f7227d339116196ccbe52b86923051441e2647d;hp=87e31e8aede6e02d8e4e8e803a25bac13cf9ec55;hpb=22344b1810548a3a75e0a7f36d23e8f8117ff633;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 87e31e8ae..6e66736a3 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1,5 +1,29 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -18,7 +42,7 @@
-
+
@@ -33,7 +57,9 @@
+
@@ -295,6 +321,23 @@
+
+
+
+
+ AS
+
+
+
+
+
+
+ __
+
+
+
+
+
@@ -342,6 +385,7 @@
+
@@ -349,13 +393,86 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+ .
+
+
+
+
+
+
+
+
+
+ :
+
+ .
+
+
+
+
+
+
+
+
+
+
+ LET
+ _
+
+
+
+
+
+
+ =
+
+
+
+
+
+
+
+ IN
+ _
+
+
+
+
+
+
+
+ LET
+ _
+
+ =
+
+ _
+ IN
+ _
+
+
+
+
- Π
+ Π
@@ -370,7 +487,7 @@
- Π
+ Π
:
@@ -386,7 +503,9 @@
- (
+
+ (
+
@@ -394,11 +513,27 @@
- →
-
+ →
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -406,14 +541,34 @@
+
- (
+
+ (
+
- →
-
- )
+ →
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ )
+
@@ -474,7 +629,7 @@
- :>
+ :>
@@ -491,7 +646,7 @@
(
- :>
+ :>
)
@@ -560,7 +715,7 @@
_
- ⇒
+ ⇒
@@ -571,7 +726,7 @@
|_
- ⇒
+ ⇒
@@ -601,7 +756,7 @@
- ⇒
+ ⇒
_
@@ -802,7 +957,7 @@
- we proved
+ we proved
_
@@ -810,6 +965,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -837,55 +1010,113 @@
)
-
+
-
-
+
+
- Consider
-
+ Consider
+ _
+
-
-
-
-
-
Rewrite
_
-
+
_
with
_
-
+
_
by
_
-
- _
- in
- _
-
- _
- and apply
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Then apply it to
_
-
+
-
+
+
+
+
+
+
+ By induction
+
+
+
+
+
+ base case:
+
+
+
+
+
+
+
+ inductive case:
+
+
+
+
+
+
+
@@ -896,7 +1127,8 @@
- Consider
+ Consider
+ _
@@ -984,6 +1216,50 @@
+
+
+
+
+
+
+
+
+
+
+ Consider
+ _
+
+
+
+
+
+
+
+
+ Let
+ _
+
+ :
+
+ _
+ such that
+ _
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -991,6 +1267,7 @@
+
@@ -1055,7 +1332,7 @@
- λ
+ λ
@@ -1070,7 +1347,7 @@
- λ
+ λ
:
@@ -1109,9 +1386,7 @@
__
-
- =
-
+ =
@@ -1221,9 +1496,9 @@
-
-
-
+
+
+
@@ -1375,7 +1650,7 @@
- >
+
@@ -1387,3 +1662,5 @@
+
+