X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=86675e553e48abf02c18c78ecf1043341445b65f;hb=083c36a4acd76127530b9af3d4c6c311f447d79b;hp=a22dc0dd332d56fcc2c4fcf3ee480792d3017c03;hpb=7ab23379f84c1b1b999a359830d333fc2925bb58;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index a22dc0dd3..86675e553 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -383,6 +383,7 @@
+
@@ -500,7 +501,9 @@
- (
+
+ (
+
@@ -509,10 +512,26 @@
→
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -520,14 +539,34 @@
+
- (
+
+ (
+
→
-
- )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ )
+
@@ -924,6 +963,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -951,55 +1008,111 @@
)
-
+
-
-
+
+
- Consider
-
+ Consider
+ _
+
-
-
-
-
-
Rewrite
_
-
+
_
with
_
-
+
_
by
_
-
- _
- in
- _
-
- _
- and apply to
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Consider
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Then apply it to
_
-
+
-
+
+
+
+
+
+
+ By induction
+
+
+
+
+
+ base case:
+
+
+
+
+
+
+
+ inductive case:
+
+
+
+
+
+
+
@@ -1010,7 +1123,8 @@
- Consider
+ Consider
+ _
@@ -1108,7 +1222,8 @@
- Consider
+ Consider
+ _
@@ -1148,6 +1263,7 @@
+
@@ -1530,7 +1646,7 @@
- >
+
@@ -1543,3 +1659,4 @@
+