X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=7e9bd1e5f085b1711a8a64458e66c7d9db7f211c;hb=9b149437fe0a9ed59e66cd87590ce6f1aed1ac64;hp=6572c0556c3f93890248c12c0fe70365fbbefaaf;hpb=5d9c64e007c6eff9447b2ef67d2a680c86c2775d;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6572c0556..7e9bd1e5f 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -40,10 +40,12 @@ which generates the toplevel element (see for instance xlink) -->
xmlns:xlink="http://www.w3.org/1999/xlink">
-
+
+
+
@@ -411,9 +413,10 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
@@ -613,7 +616,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -622,7 +628,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -638,10 +647,16 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
_
-
+
+
+
+
)
@@ -737,8 +752,8 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
@@ -751,10 +766,10 @@ which generates the toplevel element (see for instance xlink) -->
_
-
+
⇒
-
+
@@ -765,7 +780,7 @@ which generates the toplevel element (see for instance xlink) -->
|_
⇒
-
+
@@ -787,15 +802,15 @@ which generates the toplevel element (see for instance xlink) -->
_
OF
-
+
|
-
+
⇒
-
+
_
END
@@ -987,52 +1002,135 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
- We can prove
+
+
+
+
+
+
+
+ we proved
_
- _
- (explain)
+
+ _
+
+
+ (hide details)
+
-
-
-
-
-
-
-
-
-
-
-
-
-
- we proved
- _
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
+
+
+
-
- _
-
- (hide details)
+
-
-
-
-
-
+
+
+
+
+
+ we proved
+ _
+
+
+
+ _
+
+
+ (hide details)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -1040,14 +1138,14 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
@@ -1058,7 +1156,7 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
@@ -1067,7 +1165,7 @@ which generates the toplevel element (see for instance xlink) -->
- by induction on
+ by induction on
_
@@ -1099,7 +1197,7 @@ which generates the toplevel element (see for instance xlink) -->
- Case
+ Case
_
@@ -1114,7 +1212,7 @@ which generates the toplevel element (see for instance xlink) -->
- By induction hypothesis, we have:
+ By induction hypothesis, we have:
@@ -1520,6 +1618,217 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+ We have the following equality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+ =
+
+
+ =
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We have the following disequality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ [
+
+
+
+
+ ←
+
+ ]
+
+
+
+
+
+
+
+ ↑
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+ ↑
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+ →
+ β
+
+
+
+
+
+
+
+
+
+
+ →
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ≅
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1553,7 +1862,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1571,7 +1880,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1587,7 +1896,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
@@ -1621,252 +1935,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
- =
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
-
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- ∅
-
-
-
-
-
-
-
-
-
-
-
-
-
- {
-
-
-
-
-
-
-
- {
- |
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
@@ -1949,3 +2017,4 @@ which generates the toplevel element (see for instance xlink) -->
+