X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=6dce30b65a73b02bf009013469380fd523eb18a0;hb=ae326f646ef4c01b43d6da04201b427d1e175400;hp=21225aa8638e98d0211d15eccc6a4d0ee7498f47;hpb=724c03286dd6d22091490ffdd8f66120c6c09dc8;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 21225aa86..6dce30b65 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -411,9 +411,10 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
@@ -987,52 +988,71 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
+
+
+
+
+
+
+
+
+
+ We can prove
+ _
+
+
+ _
+ (explain)
+
+
+
+
+
+
+
+
+
- We can prove
+
+
+
+
+
+
+
+ we proved
_
- _
- (explain)
+
+ _
+
+
+ (hide details)
+
-
-
-
-
-
-
-
-
-
-
-
-
-
- we proved
- _
-
-
-
- _
-
- (hide details)
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
@@ -1520,6 +1540,131 @@ which generates the toplevel element (see for instance xlink) -->
+
+
+
+
+
+
+
+ [
+
+
+
+
+ ←
+
+ ]
+
+
+
+
+
+
+
+ ↑
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+ ↑
+
+
+
+
+ (
+
+ )
+
+
+
+
+
+
+
+
+
+ →
+ β
+
+
+
+
+
+
+
+
+
+
+ →
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+
+
+
+
+
+
+
+
+
+
+ ⇒
+ β
+ *
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ ≅
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1587,7 +1732,12 @@ which generates the toplevel element (see for instance xlink) -->
-
+
+
+
+
+
+
@@ -1634,7 +1784,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1652,7 +1802,12 @@ which generates the toplevel element (see for instance xlink) -->
__
- =
+
+
+
+
+
+ =
@@ -1727,7 +1882,7 @@ which generates the toplevel element (see for instance xlink) -->
-
+
@@ -1745,7 +1900,12 @@ which generates the toplevel element (see for instance xlink) -->
__
-
+
+
+
+
+
+
@@ -1769,7 +1929,12 @@ which generates the toplevel element (see for instance xlink) -->
- ∅
+
+
+
+
+
+ ∅
@@ -1783,7 +1948,12 @@ which generates the toplevel element (see for instance xlink) -->
- {
+
+
+
+
+
+ {
@@ -1800,7 +1970,12 @@ which generates the toplevel element (see for instance xlink) -->
- }
+
+
+
+
+
+ }
@@ -1811,7 +1986,12 @@ which generates the toplevel element (see for instance xlink) -->
- {
+
+
+
+
+
+ {
,
@@ -1835,7 +2015,12 @@ which generates the toplevel element (see for instance xlink) -->
- }
+
+
+
+
+
+ }
@@ -1862,11 +2047,6 @@ which generates the toplevel element (see for instance xlink) -->
-
-
-
-
-