X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fstyle%2Fmmlctop.xsl-0.14;h=1568e1da2deefc9818f6aab66c4adbf80a2c176d;hb=4020414d9bc31b545e311760045d4ce8f0645916;hp=f1ffd20fa9eb547bbb42b10ef34ea63d43e77907;hpb=fecad5c7499c396c8ff89fe7d353573991db8774;p=helm.git
diff --git a/helm/style/mmlctop.xsl-0.14 b/helm/style/mmlctop.xsl-0.14
index f1ffd20fa..1568e1da2 100755
--- a/helm/style/mmlctop.xsl-0.14
+++ b/helm/style/mmlctop.xsl-0.14
@@ -19,7 +19,7 @@
-
+
@@ -255,7 +255,7 @@ LINEAR ALGEBRA
-
+
@@ -313,7 +313,7 @@ LINEAR ALGEBRA
and $PAR_NO_IGNORE=$NO">
-
+
@@ -336,7 +336,7 @@ LINEAR ALGEBRA
-
+
@@ -457,13 +457,13 @@ HELM: Now is: -->
-
+
-
+
-
@@ -478,7 +478,7 @@ HELM: Now is: -->
-
+
@@ -496,13 +496,13 @@ HELM: Now is: -->
-
+
-
+
@@ -513,7 +513,7 @@ HELM: Now is: -->
-
+
Polar
@@ -523,7 +523,7 @@ HELM: Now is: -->
-
+
Polar
@@ -538,7 +538,7 @@ HELM: Now is: -->
-
+
@@ -546,7 +546,7 @@ HELM: Now is: -->
-
+
@@ -554,7 +554,7 @@ HELM: Now is: -->
-
+
@@ -572,7 +572,7 @@ HELM: Now is: -->
-
+
@@ -582,7 +582,7 @@ HELM: Now is: -->
-
+
@@ -593,7 +593,7 @@ HELM: Now is: -->
-
+
@@ -605,7 +605,7 @@ HELM: Now is: -->
-
+
@@ -619,7 +619,7 @@ HELM: Now is: -->
-
+
@@ -640,7 +640,7 @@ HELM: Now is: -->
-
+
@@ -689,7 +689,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -697,7 +697,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -716,7 +716,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -733,7 +733,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -754,7 +754,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
*[2]=m:arccos or *[2]=m:arctan">
-
+
@@ -764,7 +764,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -841,7 +841,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -865,7 +865,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -891,7 +891,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -906,7 +906,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -917,7 +917,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
∘
@@ -929,7 +929,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
- id
+ id
id
@@ -943,7 +943,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -951,7 +951,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -974,14 +974,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
e
@@ -992,7 +992,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1003,7 +1003,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
!
@@ -1013,7 +1013,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1023,7 +1023,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
max
@@ -1032,7 +1032,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
min
@@ -1103,7 +1103,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
$PARAM=$PAR_SAME">
-
+
@@ -1126,7 +1126,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1148,7 +1148,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
@@ -1168,7 +1168,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
@@ -1191,7 +1191,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
$PARAM=$PAR_SAME">
-
+
@@ -1214,7 +1214,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1256,7 +1256,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
+
@@ -1284,7 +1284,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1308,7 +1308,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
$PARAM=$PAR_SAME">
-
+
@@ -1331,7 +1331,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1359,7 +1359,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1368,7 +1368,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1393,7 +1393,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
$PARAM=$PAR_SAME">
-
+
@@ -1416,7 +1416,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1447,7 +1447,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
*
@@ -1463,7 +1463,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1487,7 +1487,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1495,7 +1495,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
gcd
@@ -1505,7 +1505,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
gcd
@@ -1528,7 +1528,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1550,7 +1550,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1578,7 +1578,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
∧
@@ -1598,7 +1598,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1620,7 +1620,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1648,7 +1648,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
∨
@@ -1668,7 +1668,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1689,7 +1689,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1717,7 +1717,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
⊻
@@ -1732,7 +1732,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1740,7 +1740,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
¬
@@ -1753,14 +1753,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
for all
@@ -1787,14 +1787,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
∃
@@ -1824,7 +1824,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1835,7 +1835,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1849,7 +1849,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1859,7 +1859,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
̲
@@ -1869,7 +1869,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1877,7 +1877,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1886,7 +1886,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1895,7 +1895,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1917,7 +1917,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
| m:geq | m:leq | m:equivalent]">
-
+
@@ -1929,7 +1929,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1938,7 +1938,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1947,7 +1947,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1956,7 +1956,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1965,7 +1965,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1974,7 +1974,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1983,7 +1983,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1992,7 +1992,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2004,7 +2004,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
@@ -2013,7 +2013,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
+
@@ -2027,7 +2027,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2036,7 +2036,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2045,7 +2045,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2054,7 +2054,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2063,7 +2063,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2072,7 +2072,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2081,7 +2081,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2090,7 +2090,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2109,7 +2109,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2119,7 +2119,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
ln
@@ -2130,7 +2130,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
ln
@@ -2146,7 +2146,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2157,7 +2157,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
log
@@ -2169,7 +2169,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
log
@@ -2187,7 +2187,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
log
@@ -2213,7 +2213,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2221,7 +2221,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2242,7 +2242,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2260,7 +2260,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2269,7 +2269,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2290,7 +2290,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2314,7 +2314,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2322,7 +2322,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2331,7 +2331,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2340,7 +2340,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2363,14 +2363,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
@@ -2387,7 +2387,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2425,7 +2425,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
and $PARAM=$PAR_SAME">
-
+
@@ -2448,7 +2448,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2476,7 +2476,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
⋃
@@ -2497,7 +2497,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2520,7 +2520,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2548,7 +2548,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
⋂
@@ -2570,7 +2570,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
and $PARAM=$PAR_SAME">
-
+
@@ -2593,7 +2593,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2620,7 +2620,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
\
@@ -2635,7 +2635,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2651,7 +2651,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2662,7 +2662,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2671,7 +2671,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2693,7 +2693,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2702,7 +2702,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2720,7 +2720,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2728,7 +2728,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
lim
@@ -2758,7 +2758,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
self::m:arctan]]">
-
+
@@ -2782,7 +2782,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2842,7 +2842,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2855,14 +2855,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
σ
@@ -2877,14 +2877,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
σ
@@ -2902,14 +2902,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
median
@@ -2924,14 +2924,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
mode
@@ -2946,7 +2946,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2970,7 +2970,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2987,7 +2987,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -3000,7 +3000,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -3015,14 +3015,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
det
@@ -3033,7 +3033,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -3041,7 +3041,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
T
@@ -3071,7 +3071,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
m:scalarproduct[1] | m:outerproduct[1]]">
-
+
@@ -3080,7 +3080,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -3089,7 +3089,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+