X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=67859db656d243d62babbc0a06ecc6dea80cf792;hb=0125d0d8d9844a1f0df8df3b21c1ef50e238b7fb;hp=698e8fce5f9a427cd5d22033960e8370e32447e6;hpb=aa12f8cd84908fb3757a582cadd36ef49e269a2b;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 698e8fce5..67859db65 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1,5 +1,29 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -13,6 +37,7 @@
xmlns:helm="http://www.cs.unibo.it/helm">
+
@@ -33,7 +58,9 @@
+
@@ -295,6 +322,23 @@
+
+
+
+
+ AS
+
+
+
+
+
+
+ __
+
+
+
+
+
@@ -342,6 +386,7 @@
+
@@ -355,7 +400,7 @@
-
+
@@ -370,7 +415,7 @@
-
+
:
@@ -379,13 +424,56 @@
+
+
+
+
+
+
+ LET
+ _
+
+
+
+
+
+
+ =
+
+
+
+
+
+
+
+ IN
+ _
+
+
+
+
+
+
+
+ LET
+ _
+
+ =
+
+ _
+ IN
+ _
+
+
+
+
- Π
+ Π
@@ -400,7 +488,7 @@
- Π
+ Π
:
@@ -416,7 +504,9 @@
- (
+
+ (
+
@@ -424,11 +514,27 @@
- →
-
+ →
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -436,14 +542,34 @@
+
- (
+
+ (
+
- →
-
- )
+ →
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ )
+
@@ -504,7 +630,7 @@
- :>
+ :>
@@ -521,7 +647,7 @@
(
- :>
+ :>
)
@@ -590,7 +716,7 @@
_
- ⇒
+ ⇒
@@ -601,7 +727,7 @@
|_
- ⇒
+ ⇒
@@ -631,7 +757,7 @@
- ⇒
+ ⇒
_
@@ -832,7 +958,7 @@
- we proved
+ we proved
_
@@ -840,6 +966,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -867,55 +1011,113 @@
)
-
+
-
-
+
+
- Consider
-
+ Consider
+ _
+
-
-
-
-
-
Rewrite
_
-
+
_
with
_
-
+
_
by
_
-
- _
- in
- _
-
- _
- and apply to
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Then apply it to
_
-
+
-
+
+
+
+
+
+
+ By induction
+
+
+
+
+
+ base case:
+
+
+
+
+
+
+
+ inductive case:
+
+
+
+
+
+
+
@@ -926,7 +1128,8 @@
- Consider
+ Consider
+ _
@@ -1014,6 +1217,50 @@
+
+
+
+
+
+
+
+
+
+
+ Consider
+ _
+
+
+
+
+
+
+
+
+ Let
+ _
+
+ :
+
+ _
+ such that
+ _
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1021,6 +1268,7 @@
+
@@ -1085,7 +1333,7 @@
- λ
+ λ
@@ -1100,7 +1348,7 @@
- λ
+ λ
:
@@ -1139,9 +1387,7 @@
__
-
- =
-
+ =
@@ -1405,7 +1651,7 @@
- >
+
@@ -1417,3 +1663,5 @@
+
+