X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=4a801a65402c244e03bbe273c6a4d7a7ba1709a3;hb=7c1f922d7f3b4f6538892eb4a96c9fa6e33fac0a;hp=71a424d8bb52585e46c4b9aa829eee25a43e3021;hpb=09d83294deadf767b033b1dd37bc2f902918ccc9;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 71a424d8b..4a801a654 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">
-
+
+
+
@@ -179,10 +181,54 @@ which generates the toplevel element (see for instance xlink) -->
-
+
__
- :
-
+
+
+
+
+
+
+
+
+
+ _
+
+
+ :
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+ :=
+
+
+
+
+
+ _
+ :?
+ _
+
+
+
+
+ ;
+
+
+ |-
+ ?
+ :
+
@@ -190,7 +236,7 @@ which generates the toplevel element (see for instance xlink) -->
- CORRESPONDING PROOF:
+ PROOF:
@@ -358,6 +404,61 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+ none
+
+
+ solid
+
+
+
+ ?
+ :
+ _
+
+
+
+
+
+
+
+
+ :
+
+
+ :=
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -411,10 +512,20 @@ which generates the toplevel element (see for instance xlink) -->
-
-
+
+
+
+
+
+
+
+
+
+
+
+
@@ -613,7 +724,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -622,7 +736,10 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
@@ -638,10 +755,16 @@ which generates the toplevel element (see for instance xlink) -->
(
-
+
+
+
+
_
-
+
+
+
+
)
@@ -737,7 +860,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -787,7 +910,7 @@ which generates the toplevel element (see for instance xlink) -->
_
OF
-
+
|
@@ -987,52 +1110,173 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
- We can prove
+
+
+
+
+
+
+
+ _
+
+
+ (hide details)
+
+
+
+
+
+
+ we proved
_
+
+
+
+
+
+
+
+
+
+
+ that is equivalent to
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We can prove
_
- (explain)
+
+
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- we proved
- _
-
+
_
- (hide details)
+
+ (hide details)
+
-
-
-
-
-
+
+
+
+
+ we proved
+ _
+
+
+
+
+
+
+
+
+
+
+
+ that is equivalent to
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -1040,14 +1284,14 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
@@ -1058,7 +1302,7 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
@@ -1067,7 +1311,7 @@ which generates the toplevel element (see for instance xlink) -->
- by induction on
+ by induction on
_
@@ -1099,7 +1343,7 @@ which generates the toplevel element (see for instance xlink) -->
- Case
+ Case
_
@@ -1114,7 +1358,7 @@ which generates the toplevel element (see for instance xlink) -->
- By induction hypothesis, we have:
+ By induction hypothesis, we have:
@@ -1520,32 +1764,114 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+ We have the following equality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+ =
+
+
+ =
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We have the following disequality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
-
-
- [
-
-
-
-
-
- ←
-
-
- ]
-
+
+ [
+
+
+
+
+ ←
+
+ ]
-
+
-
+
↑
@@ -1558,9 +1884,9 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
↑
@@ -1575,11 +1901,11 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
→
- β
+ β
@@ -1587,12 +1913,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
→
- β
- *
+ β
+ *
@@ -1600,11 +1926,11 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
⇒
- β
+ β
@@ -1612,12 +1938,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
⇒
- β
- *
+ β
+ *
@@ -1625,7 +1951,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1633,9 +1959,9 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
≅
@@ -1643,7 +1969,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1682,7 +2008,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1700,7 +2026,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1716,7 +2042,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
@@ -1750,252 +2081,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
- =
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
-
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- ∅
-
-
-
-
-
-
-
-
-
-
-
-
-
- {
-
-
-
-
-
-
-
- {
- |
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
@@ -2053,7 +2138,16 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
+
+
+
+
@@ -2078,3 +2172,4 @@ which generates the toplevel element (see for instance xlink) -->
+