X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=a22dc0dd332d56fcc2c4fcf3ee480792d3017c03;hb=4e8b137b58ec6763785b8ee490ee8cd6cb77b5bf;hp=0a11b499174ebee7d7f50486242b48ec60ccab1b;hpb=039f58232964e627868ec21f7c1e64c843204c75;p=helm.git
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 0a11b4991..a22dc0dd3 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -1,5 +1,29 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
@@ -295,6 +319,23 @@
+
+
+
+
+ AS
+
+
+
+
+
+
+ __
+
+
+
+
+
@@ -349,13 +390,86 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+ .
+
+
+
+
+
+
+
+
+
+ :
+
+ .
+
+
+
+
+
+
+
+
+
+
+ LET
+ _
+
+
+
+
+
+
+ =
+
+
+
+
+
+
+
+ IN
+ _
+
+
+
+
+
+
+
+ LET
+ _
+
+ =
+
+ _
+ IN
+ _
+
+
+
+
- Π
+ Π
@@ -370,7 +484,7 @@
- Π
+ Π
:
@@ -394,7 +508,7 @@
- →
+ →
@@ -411,7 +525,7 @@
(
- →
+ →
)
@@ -474,7 +588,7 @@
- :>
+ :>
@@ -491,7 +605,7 @@
(
- :>
+ :>
)
@@ -560,7 +674,7 @@
_
- ⇒
+ ⇒
@@ -571,7 +685,7 @@
|_
- ⇒
+ ⇒
@@ -601,7 +715,7 @@
- ⇒
+ ⇒
_
@@ -802,7 +916,7 @@
- we proved
+ we proved
_
@@ -984,6 +1098,49 @@
+
+
+
+
+
+
+
+
+
+
+ Consider
+
+
+
+
+
+
+
+
+ Let
+ _
+
+ :
+
+ _
+ such that
+ _
+ (
+
+ )
+ _
+
+
+
+
+
+
+
+
+
+
+
+
ERROR
@@ -1015,7 +1172,7 @@
- we get
+ we get
_
@@ -1033,7 +1190,7 @@
- we get
+ we get
_
@@ -1055,7 +1212,7 @@
- λ
+ λ
@@ -1070,7 +1227,7 @@
- λ
+ λ
:
@@ -1109,9 +1266,7 @@
__
-
- =
-
+ =
@@ -1387,3 +1542,4 @@
+