X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=7e9bd1e5f085b1711a8a64458e66c7d9db7f211c;hb=4c9123ced31cede42e5cc1e19d701a6f6e5e9d6b;hp=6dce30b65a73b02bf009013469380fd523eb18a0;hpb=845ec24db2f3aba5d3a4a991f2604b5b87283119;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 6dce30b65..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">
-
+
+
+
@@ -614,7 +616,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -623,7 +628,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -639,10 +647,16 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
_
-
+
+
+
+
)
@@ -1000,7 +1014,7 @@ which generates the toplevel element (see for instance xlink) -->
- We can prove
+ We can prove
_
@@ -1026,7 +1040,71 @@ which generates the toplevel element (see for instance xlink) -->
- we proved
+ we proved
+ _
+
+
+
+ _
+
+
+ (hide details)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ we proved
_
@@ -1060,14 +1138,14 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
@@ -1078,7 +1156,7 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
@@ -1087,7 +1165,7 @@ which generates the toplevel element (see for instance xlink) -->
- by induction on
+ by induction on
_
@@ -1119,7 +1197,7 @@ which generates the toplevel element (see for instance xlink) -->
- Case
+ Case
_
@@ -1134,7 +1212,7 @@ which generates the toplevel element (see for instance xlink) -->
- By induction hypothesis, we have:
+ By induction hypothesis, we have:
@@ -1540,6 +1618,92 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+ We have the following equality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+ =
+
+
+ =
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We have the following disequality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
@@ -1549,7 +1713,7 @@ which generates the toplevel element (see for instance xlink) -->
[
-
+
←
@@ -1559,7 +1723,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
↑
@@ -1574,7 +1738,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
↑
@@ -1591,11 +1755,11 @@ which generates the toplevel element (see for instance xlink) -->
-
+
→
- β
+ β
@@ -1603,12 +1767,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
→
- β
- *
+ β
+ *
@@ -1616,11 +1780,11 @@ which generates the toplevel element (see for instance xlink) -->
-
+
⇒
- β
+ β
@@ -1628,12 +1792,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
⇒
- β
- *
+ β
+ *
@@ -1649,7 +1813,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
≅
@@ -1698,7 +1862,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1716,7 +1880,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1771,282 +1935,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
-
-
-
-
-
- =
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- ∅
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- {
-
-
-
-
-
-
-
- {
- |
-
-
-
-
-
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
@@ -2129,3 +2017,4 @@ which generates the toplevel element (see for instance xlink) -->
+