X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlctop.xsl-0.14;h=1568e1da2deefc9818f6aab66c4adbf80a2c176d;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=4ab889155b1293fd5cfab544a816643e7889c290;hpb=5d9c64e007c6eff9447b2ef67d2a680c86c2775d;p=helm.git diff --git a/helm/style/mmlctop.xsl-0.14 b/helm/style/mmlctop.xsl-0.14 index 4ab889155..1568e1da2 100755 --- a/helm/style/mmlctop.xsl-0.14 +++ b/helm/style/mmlctop.xsl-0.14 @@ -19,7 +19,7 @@ - + @@ -37,7 +37,11 @@ + + + - + @@ -299,15 +303,17 @@ LINEAR ALGEBRA + - + @@ -326,16 +332,18 @@ LINEAR ALGEBRA + @@ -420,22 +428,42 @@ LINEAR ALGEBRA - + + + + - + + + + + + + + + + + + + + + + - + - + - @@ -450,7 +478,7 @@ LINEAR ALGEBRA - + @@ -468,13 +496,13 @@ LINEAR ALGEBRA - + - + @@ -485,7 +513,7 @@ LINEAR ALGEBRA - + Polar @@ -495,7 +523,7 @@ LINEAR ALGEBRA - + Polar @@ -507,23 +535,44 @@ LINEAR ALGEBRA - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - + @@ -533,7 +582,7 @@ LINEAR ALGEBRA - + @@ -544,7 +593,7 @@ LINEAR ALGEBRA - + @@ -556,7 +605,7 @@ LINEAR ALGEBRA - + @@ -564,21 +613,22 @@ LINEAR ALGEBRA + + + + + + + + + + + - - - - - - - - - - - @@ -590,7 +640,7 @@ LINEAR ALGEBRA - + @@ -639,7 +689,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -647,7 +697,7 @@ 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,7 +733,7 @@ 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,7 +865,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -841,7 +891,7 @@ 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,7 +917,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -879,7 +929,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - id + id id @@ -893,7 +943,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -901,7 +951,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -924,14 +974,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + e @@ -942,7 +992,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -953,7 +1003,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ! @@ -963,7 +1013,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -973,7 +1023,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + max @@ -982,7 +1032,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + min @@ -1053,7 +1103,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> $PARAM=$PAR_SAME"> - + @@ -1076,7 +1126,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1098,7 +1148,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - @@ -1118,7 +1168,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - @@ -1141,7 +1191,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> $PARAM=$PAR_SAME"> - + @@ -1164,7 +1214,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1206,7 +1256,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + + @@ -1234,7 +1284,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1258,7 +1308,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> $PARAM=$PAR_SAME"> - + @@ -1281,7 +1331,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1309,7 +1359,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1318,7 +1368,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1343,7 +1393,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> $PARAM=$PAR_SAME"> - + @@ -1366,7 +1416,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1397,7 +1447,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + * @@ -1413,7 +1463,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1437,7 +1487,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1445,7 +1495,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + gcd @@ -1455,7 +1505,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + gcd @@ -1478,7 +1528,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1500,7 +1550,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1528,7 +1578,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1548,7 +1598,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1570,7 +1620,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1598,7 +1648,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1618,7 +1668,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1639,7 +1689,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1667,7 +1717,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1682,7 +1732,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1690,7 +1740,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ¬ @@ -1703,14 +1753,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + for all @@ -1737,14 +1787,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + @@ -1774,7 +1824,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1785,7 +1835,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1799,7 +1849,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1809,7 +1859,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ̲ @@ -1819,7 +1869,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1827,7 +1877,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1836,7 +1886,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1845,7 +1895,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1867,7 +1917,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> | m:geq | m:leq | m:equivalent]"> - + @@ -1879,7 +1929,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1888,7 +1938,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1897,7 +1947,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1906,7 +1956,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1915,7 +1965,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1924,7 +1974,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1933,7 +1983,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1942,7 +1992,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1954,7 +2004,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - @@ -1963,7 +2013,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + + @@ -1977,7 +2027,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1986,7 +2036,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1995,7 +2045,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2004,7 +2054,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2013,7 +2063,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2022,7 +2072,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2031,7 +2081,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2040,7 +2090,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2059,7 +2109,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2069,7 +2119,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ln @@ -2080,7 +2130,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ln @@ -2096,7 +2146,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2107,7 +2157,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + log @@ -2119,7 +2169,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + log @@ -2137,7 +2187,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + log @@ -2163,7 +2213,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2171,7 +2221,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2192,7 +2242,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2210,7 +2260,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2219,7 +2269,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2240,7 +2290,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2264,7 +2314,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2272,7 +2322,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2281,7 +2331,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2290,7 +2340,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2313,14 +2363,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + @@ -2337,7 +2387,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2375,7 +2425,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> and $PARAM=$PAR_SAME"> - + @@ -2398,7 +2448,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2426,7 +2476,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2447,7 +2497,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2470,7 +2520,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2498,7 +2548,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2520,7 +2570,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> and $PARAM=$PAR_SAME"> - + @@ -2543,7 +2593,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2570,7 +2620,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + \ @@ -2585,7 +2635,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2601,7 +2651,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2612,7 +2662,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2621,7 +2671,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2643,7 +2693,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2652,7 +2702,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2670,7 +2720,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2678,7 +2728,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + lim @@ -2708,7 +2758,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> self::m:arctan]]"> - + @@ -2732,7 +2782,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2792,7 +2842,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2805,14 +2855,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + σ @@ -2827,14 +2877,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + σ @@ -2852,14 +2902,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + median @@ -2874,14 +2924,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + mode @@ -2896,7 +2946,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2920,7 +2970,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2937,7 +2987,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2950,7 +3000,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2965,14 +3015,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + det @@ -2983,7 +3033,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2991,7 +3041,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + T @@ -3021,7 +3071,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> m:scalarproduct[1] | m:outerproduct[1]]"> - + @@ -3030,7 +3080,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -3039,7 +3089,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - +