X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6dce30b65a73b02bf009013469380fd523eb18a0;hb=5735143021bfe2b270f57e115d109a1f876faccc;hp=bb13c876ebcd93bf38997b2c190d2a0b3e258747;hpb=1fff0186531410297e970ba862947b2cbd539fb5;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index bb13c876e..6dce30b65 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -373,21 +373,27 @@ which generates the toplevel element (see for instance xlink) -->
-
- :
+
+
+ :
+
+
+
-
- :
-
+
+
+ :
+
+
@@ -405,9 +411,10 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
@@ -417,7 +424,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
@@ -433,7 +440,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+ ∀
:
@@ -731,8 +738,8 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
@@ -745,10 +752,10 @@ which generates the toplevel element (see for instance xlink) -->
_
-
+
⇒
-
+
@@ -759,7 +766,7 @@ which generates the toplevel element (see for instance xlink) -->
|_
⇒
-
+
@@ -781,15 +788,15 @@ which generates the toplevel element (see for instance xlink) -->
_
OF
-
+
|
-
+
⇒
-
+
_
END
@@ -981,48 +988,71 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
- We can prove
- _
-
-
-
- _
-
- (explain)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- we proved
- _
-
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
+
+
+
-
- _
-
- (hide details)
+
-
-
-
-
-
+
+
+
+
+
+ we proved
+ _
+
+
+
+ _
+
+
+ (hide details)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -1043,15 +1073,12 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
- We prove
+ We prove
_
@@ -1060,9 +1087,9 @@ which generates the toplevel element (see for instance xlink) -->
- by induction on
+ by induction on
_
-
@@ -1070,12 +1097,13 @@ which generates the toplevel element (see for instance xlink) -->
- _
-
+
+
+
@@ -1091,7 +1119,7 @@ which generates the toplevel element (see for instance xlink) -->
- Case
+ Case
_
@@ -1105,7 +1133,9 @@ which generates the toplevel element (see for instance xlink) -->
- By induction hypothesis, we have:
+
+ By induction hypothesis, we have:
+
@@ -1125,7 +1155,9 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
@@ -1155,6 +1187,7 @@ which generates the toplevel element (see for instance xlink) -->
+
@@ -1173,8 +1206,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
@@ -1278,7 +1309,7 @@ which generates the toplevel element (see for instance xlink) -->
- Then apply it to
+ Then apply it to
_
@@ -1308,7 +1339,7 @@ which generates the toplevel element (see for instance xlink) -->
- In particular, we have
+ In particular, we have
@@ -1343,8 +1374,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
@@ -1367,7 +1396,7 @@ which generates the toplevel element (see for instance xlink) -->
- We proceed by cases to prove
+ We proceed by cases to prove
_
@@ -1376,7 +1405,7 @@ which generates the toplevel element (see for instance xlink) -->
- Left: suppose
+ Left: suppose
_
(
@@ -1388,8 +1417,8 @@ which generates the toplevel element (see for instance xlink) -->
- _
+ _
@@ -1397,7 +1426,7 @@ which generates the toplevel element (see for instance xlink) -->
- Right: suppose
+ Right: suppose
_
(
@@ -1416,7 +1445,6 @@ which generates the toplevel element (see for instance xlink) -->
-
@@ -1439,11 +1467,11 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
_
- by cases:
+ by cases:
@@ -1493,7 +1521,7 @@ which generates the toplevel element (see for instance xlink) -->
:
_
- such that
+ such that
_
(
@@ -1512,6 +1540,131 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+
+ [
+
+
+
+
+ ←
+
+ ]
+
+
+
+
+
+
+
+ ↑
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+ ↑
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+ →
+ β
+
+
+
+
+
+
+
+
+
+
+ →
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ≅
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1545,7 +1698,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1563,7 +1716,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1579,7 +1732,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
@@ -1626,7 +1784,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1644,7 +1802,12 @@ which generates the toplevel element (see for instance xlink) -->
__
- =
+
+
+
+
+
+ =
@@ -1673,43 +1836,43 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
-
+
@@ -1719,7 +1882,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1737,9 +1900,12 @@ which generates the toplevel element (see for instance xlink) -->
__
-
-
-
+
+
+
+
+
+
@@ -1763,9 +1929,12 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
+
+
+
+
+
+ ∅
@@ -1779,7 +1948,12 @@ which generates the toplevel element (see for instance xlink) -->
- {
+
+
+
+
+
+ {
@@ -1796,7 +1970,12 @@ which generates the toplevel element (see for instance xlink) -->
- }
+
+
+
+
+
+ }
@@ -1807,7 +1986,12 @@ which generates the toplevel element (see for instance xlink) -->
- {
+
+
+
+
+
+ {
,
@@ -1831,7 +2015,12 @@ which generates the toplevel element (see for instance xlink) -->
- }
+
+
+
+
+
+ }
@@ -1858,11 +2047,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
@@ -1945,6 +2129,3 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-