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=aca072bb645556ccdaea01b5fde52bf5196ec2e3;hpb=b205c1fb5ec671d31e051a9a2f0e534b4e393452;p=helm.git
diff --git a/helm/style/mmlctop.xsl-0.14 b/helm/style/mmlctop.xsl-0.14
index aca072bb6..1568e1da2 100755
--- a/helm/style/mmlctop.xsl-0.14
+++ b/helm/style/mmlctop.xsl-0.14
@@ -19,7 +19,8 @@
-
+
+
@@ -36,7 +37,11 @@
+
+
+
-
+
@@ -298,15 +303,17 @@ LINEAR ALGEBRA
+
-
+
@@ -325,16 +332,18 @@ LINEAR ALGEBRA
+
@@ -357,7 +366,7 @@ LINEAR ALGEBRA
+
-
+
i
@@ -373,7 +382,7 @@ LINEAR ALGEBRA
+
-
+
i
@@ -399,7 +408,7 @@ LINEAR ALGEBRA
Polar
-
+
@@ -410,7 +419,7 @@ LINEAR ALGEBRA
Polar
-
+
@@ -419,22 +428,42 @@ LINEAR ALGEBRA
-
+
+
+
+
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
+
-
+
-
@@ -444,12 +473,12 @@ LINEAR ALGEBRA
+
-
+
i
-
+
@@ -460,20 +489,20 @@ LINEAR ALGEBRA
+
-
+
i
-
+
-
+
@@ -484,9 +513,9 @@ LINEAR ALGEBRA
-
+
Polar
-
+
@@ -494,10 +523,10 @@ LINEAR ALGEBRA
-
+
Polar
-
+
@@ -506,23 +535,44 @@ LINEAR ALGEBRA
-
-
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
+
@@ -532,7 +582,7 @@ LINEAR ALGEBRA
-
+
@@ -543,7 +593,7 @@ LINEAR ALGEBRA
-
+
@@ -555,7 +605,7 @@ LINEAR ALGEBRA
-
+
@@ -563,21 +613,22 @@ LINEAR ALGEBRA
+
+
+
+
+
+
+
+
+
+
+
-
-
-
-
-
-
-
-
-
-
-
@@ -589,7 +640,7 @@ LINEAR ALGEBRA
-
+
@@ -638,7 +689,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -646,11 +697,10 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+
@@ -666,7 +716,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -683,12 +733,12 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
@@ -704,7 +754,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
*[2]=m:arccos or *[2]=m:arctan">
-
+
@@ -714,7 +764,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -791,7 +841,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -815,12 +865,12 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+ Λ
+
@@ -841,12 +891,12 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
@@ -856,7 +906,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -867,11 +917,10 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+ ∘
@@ -880,7 +929,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
- id
+ id
id
@@ -894,17 +943,15 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
-
+ ⌊
-
+
@@ -920,23 +967,21 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
-
-
+ ⌊
-
+
-
+
e
@@ -947,7 +992,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -958,7 +1003,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
!
@@ -968,7 +1013,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -978,7 +1023,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
max
@@ -987,7 +1032,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
min
@@ -1058,7 +1103,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
$PARAM=$PAR_SAME">
-
+
@@ -1081,7 +1126,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1103,7 +1148,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
@@ -1123,7 +1168,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
@@ -1146,7 +1191,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
$PARAM=$PAR_SAME">
-
+
@@ -1169,7 +1214,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1211,7 +1256,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
+
@@ -1239,7 +1284,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1263,7 +1308,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
$PARAM=$PAR_SAME">
-
+
@@ -1286,7 +1331,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1314,7 +1359,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1323,7 +1368,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1348,7 +1393,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
$PARAM=$PAR_SAME">
-
+
@@ -1371,7 +1416,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1398,11 +1443,11 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
*
@@ -1418,7 +1463,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1442,7 +1487,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1450,7 +1495,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
gcd
@@ -1460,7 +1505,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
gcd
@@ -1483,7 +1528,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1505,7 +1550,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1533,11 +1578,10 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+ ∧
@@ -1554,7 +1598,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1576,7 +1620,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1604,11 +1648,10 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+ ∨
@@ -1625,7 +1668,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1646,7 +1689,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1674,11 +1717,10 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+ ⊻
@@ -1690,7 +1732,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1698,10 +1740,10 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+ ¬
@@ -1711,14 +1753,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
for all
@@ -1745,18 +1787,17 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
-
-
+ ∃
@@ -1783,7 +1824,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1794,7 +1835,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1808,7 +1849,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1818,18 +1859,17 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+ ̲
-
+
@@ -1837,7 +1877,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1846,7 +1886,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1855,7 +1895,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -1877,7 +1917,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
| m:geq | m:leq | m:equivalent]">
-
+
@@ -1889,74 +1929,74 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+ ≠
-
+
-
+ ≊
-
+
-
+ →
-
+
-
+ ⇒
-
+
-
+ ∈
-
+
-
+ ∉
-
+
-
+ ⊄
-
+
-
+ ⊈
@@ -1964,7 +2004,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
@@ -1973,7 +2013,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
+
@@ -1987,25 +2027,25 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+ ⊆
-
+
-
+ ⊂
-
+
@@ -2014,7 +2054,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2023,7 +2063,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2032,29 +2072,29 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+ ≥
-
+
-
+ ≤
-
+
-
+ ≡
@@ -2069,7 +2109,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2079,7 +2119,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
ln
@@ -2090,13 +2130,13 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
ln
-
+
@@ -2106,7 +2146,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2117,7 +2157,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
log
@@ -2129,7 +2169,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
log
@@ -2147,7 +2187,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
log
@@ -2156,7 +2196,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2173,7 +2213,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2181,7 +2221,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2202,7 +2242,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2220,7 +2260,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2229,7 +2269,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2250,7 +2290,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2274,7 +2314,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2282,7 +2322,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2291,7 +2331,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2300,7 +2340,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2323,18 +2363,18 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
-
+ Δ
2
@@ -2347,7 +2387,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2385,7 +2425,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
and $PARAM=$PAR_SAME">
-
+
@@ -2408,7 +2448,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2436,11 +2476,10 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+ ⋃
@@ -2458,7 +2497,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2481,7 +2520,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2509,11 +2548,10 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
-
+ ⋂
@@ -2532,7 +2570,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
and $PARAM=$PAR_SAME">
-
+
@@ -2555,7 +2593,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2582,7 +2620,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
\
@@ -2597,7 +2635,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2613,7 +2651,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2624,20 +2662,20 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+ ∑
-
+
-
+ ∏
@@ -2655,20 +2693,20 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+ ∑
-
+
-
+ ∏
@@ -2682,7 +2720,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2690,14 +2728,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
lim
-
+ →
@@ -2720,7 +2758,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
self::m:arctan]]">
-
+
@@ -2733,7 +2771,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2744,7 +2782,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2804,7 +2842,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2817,18 +2855,17 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
-
-
+ σ
@@ -2840,18 +2877,17 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
-
-
+ σ
@@ -2866,14 +2902,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
median
@@ -2888,14 +2924,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
mode
@@ -2910,7 +2946,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2934,7 +2970,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2951,7 +2987,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2964,7 +3000,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -2979,14 +3015,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+
det
@@ -2997,7 +3033,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
@@ -3005,7 +3041,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
T
@@ -3035,7 +3071,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
m:scalarproduct[1] | m:outerproduct[1]]">
-
+
@@ -3044,16 +3080,16 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
-
+
-
+ ⨯
-
+