X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6ab6ffe1fcfbc51f201b94adcee89a14ff22d278;hb=1cfcea66d7394a785ec439cd6b03497b276918c4;hp=d0c8555b39ac48df5c4a91c1469350ffcff0dfdb;hpb=a0da07547d92d5bcb9f9eac2399ccb6b700b9d03;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index d0c8555b3..6ab6ffe1f 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
+
+
+
+ ?
+ :
+ _
+
+
+
+
+
+
+
+
+ :
+
+
+ :=
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -412,9 +513,19 @@ 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) -->
(
-
+
+
+
+
_
-
+
+
+
+
)
@@ -987,58 +1110,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)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -1046,14 +1246,14 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
@@ -1064,7 +1264,7 @@ which generates the toplevel element (see for instance xlink) -->
- We prove
+ We prove
_
@@ -1073,7 +1273,7 @@ which generates the toplevel element (see for instance xlink) -->
- by induction on
+ by induction on
_
@@ -1105,7 +1305,7 @@ which generates the toplevel element (see for instance xlink) -->
- Case
+ Case
_
@@ -1120,7 +1320,7 @@ which generates the toplevel element (see for instance xlink) -->
- By induction hypothesis, we have:
+ By induction hypothesis, we have:
@@ -1526,6 +1726,92 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+ We have the following equality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+ =
+
+
+ =
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ We have the following disequality chain:
+
+
+
+
+
+
+
+
+
+
+
+ _
+
+
+
+
+ _
+
+
+
+
+
+
+
+
+
+
+ __
+
+
+
+
+
+
+
+
@@ -1535,9 +1821,9 @@ which generates the toplevel element (see for instance xlink) -->
[
-
+
-
+
←
]
@@ -1545,9 +1831,9 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
↑
@@ -1560,9 +1846,9 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
↑
@@ -1577,11 +1863,11 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
→
- β
+ β
@@ -1589,12 +1875,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
→
- β
- *
+ β
+ *
@@ -1602,11 +1888,11 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
⇒
- β
+ β
@@ -1614,12 +1900,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
⇒
- β
- *
+ β
+ *
@@ -1627,7 +1913,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1635,9 +1921,9 @@ which generates the toplevel element (see for instance xlink) -->
-
+
-
+
≅
@@ -1645,7 +1931,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1684,7 +1970,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1702,7 +1988,7 @@ which generates the toplevel element (see for instance xlink) -->
- we get
+ we get
_
@@ -1720,7 +2006,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1757,282 +2043,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
-
-
-
-
-
- =
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- (
-
-
-
-
-
-
-
-
- __
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- )
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- ∅
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- {
-
-
-
-
-
-
-
- {
- |
-
-
-
-
-
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
- {
-
-
- ,
-
-
-
-
-
-
-
-
-
-
-
-
-
- }
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
@@ -2115,3 +2125,4 @@ which generates the toplevel element (see for instance xlink) -->
+