X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fstyle%2Fmmlextension.xsl;h=eb928b41f183b9f8685525b2898a883ed642a766;hb=e4ea08104e12e2d9e546f37e2d4fbb4febe75d29;hp=8566c972630e3435160cb4cc772c425169edb34b;hpb=f757483a6beb4ed12c9959c07567e8891a2b3048;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 8566c9726..eb928b41f 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -44,6 +44,8 @@ which generates the toplevel element (see for instance xlink) -->
+
+
@@ -371,21 +373,27 @@ which generates the toplevel element (see for instance xlink) -->
-
- :
+
+
+ :
+
+
+
-
- :
-
+
+
+ :
+
+
@@ -403,9 +411,10 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
@@ -415,7 +424,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
@@ -431,7 +440,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
:
@@ -729,8 +738,8 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
@@ -743,10 +752,10 @@ which generates the toplevel element (see for instance xlink) -->
_
-
+
⇒
-
+
@@ -757,7 +766,7 @@ which generates the toplevel element (see for instance xlink) -->
|_
⇒
-
+
@@ -779,15 +788,15 @@ which generates the toplevel element (see for instance xlink) -->
_
OF
-
+
|
-
+
⇒
-
+
_
END
@@ -979,6 +988,31 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
@@ -990,13 +1024,22 @@ which generates the toplevel element (see for instance xlink) -->
- we proved
+ we proved
_
+
+
+ _
+
+
+ (hide details)
+
+
+
@@ -1017,15 +1060,12 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
- We prove
+ We prove
_
@@ -1034,9 +1074,9 @@ which generates the toplevel element (see for instance xlink) -->
- by induction on
+ by induction on
_
-
@@ -1044,12 +1084,13 @@ which generates the toplevel element (see for instance xlink) -->
- _
-
+
+
+
@@ -1065,7 +1106,7 @@ which generates the toplevel element (see for instance xlink) -->
- Case
+ Case
_
@@ -1079,7 +1120,9 @@ which generates the toplevel element (see for instance xlink) -->
- By induction hypothesis, we have:
+
+ By induction hypothesis, we have:
+
@@ -1099,7 +1142,9 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
@@ -1129,6 +1174,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -1147,8 +1193,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
@@ -1252,7 +1296,7 @@ which generates the toplevel element (see for instance xlink) -->
- Then apply it to
+ Then apply it to
_
@@ -1282,7 +1326,7 @@ which generates the toplevel element (see for instance xlink) -->
- In particular, we have
+ In particular, we have
@@ -1317,8 +1361,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
@@ -1341,7 +1383,7 @@ which generates the toplevel element (see for instance xlink) -->
- We proceed by cases to prove
+ We proceed by cases to prove
_
@@ -1350,7 +1392,7 @@ which generates the toplevel element (see for instance xlink) -->
- Left: suppose
+ Left: suppose
_
(
@@ -1362,8 +1404,8 @@ which generates the toplevel element (see for instance xlink) -->
- _
+ _
@@ -1371,7 +1413,7 @@ which generates the toplevel element (see for instance xlink) -->
- Right: suppose
+ Right: suppose
_
(
@@ -1390,7 +1432,6 @@ which generates the toplevel element (see for instance xlink) -->
-
@@ -1413,11 +1454,11 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
_
- by cases:
+ by cases:
@@ -1467,7 +1508,7 @@ which generates the toplevel element (see for instance xlink) -->
:
_
- such that
+ such that
_
(
@@ -1486,6 +1527,131 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+
+ [
+
+
+
+
+ ←
+
+ ]
+
+
+
+
+
+
+
+ ↑
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+ ↑
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+ →
+ β
+
+
+
+
+
+
+
+
+
+
+ →
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ≅
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1519,7 +1685,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1537,7 +1703,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1553,7 +1719,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
@@ -1600,7 +1771,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1618,7 +1789,12 @@ which generates the toplevel element (see for instance xlink) -->
__
- =
+
+
+
+
+
+ =
@@ -1647,43 +1823,43 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -1693,7 +1869,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1711,9 +1887,12 @@ which generates the toplevel element (see for instance xlink) -->
__
-
-
-
+
+
+
+
+
+
@@ -1737,9 +1916,12 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
+
+
+
+
+
+ ∅
@@ -1753,7 +1935,12 @@ which generates the toplevel element (see for instance xlink) -->
- {
+
+
+
+
+
+ {
@@ -1770,7 +1957,12 @@ which generates the toplevel element (see for instance xlink) -->
- }
+
+
+
+
+
+ }
@@ -1781,7 +1973,12 @@ which generates the toplevel element (see for instance xlink) -->
- {
+
+
+
+
+
+ {
,
@@ -1805,7 +2002,12 @@ which generates the toplevel element (see for instance xlink) -->
- }
+
+
+
+
+
+ }
@@ -1832,11 +2034,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
@@ -1919,6 +2116,3 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-