X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=67859db656d243d62babbc0a06ecc6dea80cf792;hb=c5d44ddea495d6f20c05267e0ebd158972a21987;hp=24c4bdbe50a2883e2ceaf2ea33f698f37bff29a8;hpb=138e51f3dc9bd6a42b84e45f9bf2c681cd411393;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 24c4bdbe5..67859db65 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -37,6 +37,7 @@
xmlns:helm="http://www.cs.unibo.it/helm">
+
@@ -57,7 +58,9 @@
+
@@ -383,6 +386,7 @@
+
@@ -500,7 +504,9 @@
- (
+
+ (
+
@@ -509,10 +515,26 @@
→
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -520,14 +542,34 @@
+
- (
+
+ (
+
→
-
- )
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ )
+
@@ -924,6 +966,24 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -951,55 +1011,113 @@
)
-
+
-
-
+
+
- Consider
-
+ Consider
+ _
+
-
-
-
-
-
Rewrite
_
-
+
_
with
_
-
+
_
by
_
-
- _
- in
- _
-
- _
- and apply to
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ Then apply it to
_
-
+
-
+
+
+
+
+
+
+ By induction
+
+
+
+
+
+ base case:
+
+
+
+
+
+
+
+ inductive case:
+
+
+
+
+
+
+
@@ -1010,7 +1128,8 @@
- Consider
+ Consider
+ _
@@ -1098,6 +1217,50 @@
+
+
+
+
+
+
+
+
+
+
+ Consider
+ _
+
+
+
+
+
+
+
+
+ Let
+ _
+
+ :
+
+ _
+ such that
+ _
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1105,6 +1268,7 @@
+
@@ -1223,9 +1387,7 @@
__
-
- =
-
+ =
@@ -1489,7 +1651,7 @@
- >
+
@@ -1502,3 +1664,4 @@
+