X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6e66736a32aeb8e1fc866033a8091fc511f028f7;hb=e1d232bab1b061d9098fd666ca24bed84b38f99e;hp=f9dcfae51b6dd0ee8cb0809ad77fd7398982ea7a;hpb=a67544c0aa4c12b6b900345d16d43d0ee20eccf1;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index f9dcfae51..6e66736a3 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -57,7 +57,9 @@
+
@@ -383,7 +385,7 @@
-
+
@@ -504,7 +506,7 @@
(
-
+
@@ -520,12 +522,12 @@
-
+
-
+
@@ -546,7 +548,7 @@
(
-
+
→
@@ -556,12 +558,12 @@
-
+
-
+
@@ -963,6 +965,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -990,55 +1010,113 @@
)
-
+
-
-
+
+
- Consider
-
+ Consider
+ _
+
-
-
-
-
-
Rewrite
_
-
+
_
with
_
-
+
_
by
_
-
- _
- in
- _
-
- _
- and apply to
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Then apply it to
_
-
+
-
+
+
+
+
+
+
+ By induction
+
+
+
+
+
+ base case:
+
+
+
+
+
+
+
+ inductive case:
+
+
+
+
+
+
+
@@ -1049,7 +1127,8 @@
- Consider
+ Consider
+ _
@@ -1147,7 +1226,8 @@
- Consider
+ Consider
+ _
@@ -1187,6 +1267,7 @@
+