X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlctop.xsl-0.14;h=1568e1da2deefc9818f6aab66c4adbf80a2c176d;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=693f962a387a15db6903ef6cf9bbeb12d57801ff;hpb=aa5fbd45fd757d44f9a0ea4d2c6b8b24d0dbee9a;p=helm.git diff --git a/helm/style/mmlctop.xsl-0.14 b/helm/style/mmlctop.xsl-0.14 index 693f962a3..1568e1da2 100755 --- a/helm/style/mmlctop.xsl-0.14 +++ b/helm/style/mmlctop.xsl-0.14 @@ -19,7 +19,7 @@ - + @@ -37,7 +37,11 @@ + + + - + @@ -309,7 +313,7 @@ LINEAR ALGEBRA and $PAR_NO_IGNORE=$NO"> - + @@ -332,7 +336,7 @@ LINEAR ALGEBRA - + @@ -453,13 +457,13 @@ HELM: Now is: --> - + - + - @@ -474,7 +478,7 @@ HELM: Now is: --> - + @@ -492,13 +496,13 @@ HELM: Now is: --> - + - + @@ -509,7 +513,7 @@ HELM: Now is: --> - + Polar @@ -519,7 +523,7 @@ HELM: Now is: --> - + Polar @@ -534,7 +538,7 @@ HELM: Now is: --> - + @@ -542,7 +546,7 @@ HELM: Now is: --> - + @@ -550,7 +554,7 @@ HELM: Now is: --> - + @@ -568,7 +572,7 @@ HELM: Now is: --> - + @@ -578,7 +582,7 @@ HELM: Now is: --> - + @@ -589,7 +593,7 @@ HELM: Now is: --> - + @@ -601,7 +605,7 @@ HELM: Now is: --> - + @@ -615,7 +619,7 @@ HELM: Now is: --> - + @@ -636,7 +640,7 @@ HELM: Now is: --> - + @@ -685,7 +689,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -693,7 +697,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -712,7 +716,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -729,7 +733,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -750,7 +754,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> *[2]=m:arccos or *[2]=m:arctan"> - + @@ -760,7 +764,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -837,7 +841,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -861,7 +865,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -887,7 +891,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -902,7 +906,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -913,7 +917,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -925,7 +929,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - id + id id @@ -939,7 +943,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -947,7 +951,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -970,14 +974,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + e @@ -988,7 +992,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -999,7 +1003,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ! @@ -1009,7 +1013,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1019,7 +1023,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + max @@ -1028,7 +1032,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + min @@ -1099,7 +1103,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> $PARAM=$PAR_SAME"> - + @@ -1122,7 +1126,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1144,7 +1148,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - @@ -1164,7 +1168,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - @@ -1187,7 +1191,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> $PARAM=$PAR_SAME"> - + @@ -1210,7 +1214,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1252,7 +1256,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + + @@ -1280,7 +1284,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1304,7 +1308,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> $PARAM=$PAR_SAME"> - + @@ -1327,7 +1331,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1355,7 +1359,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1364,7 +1368,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1389,7 +1393,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> $PARAM=$PAR_SAME"> - + @@ -1412,7 +1416,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1443,7 +1447,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + * @@ -1459,7 +1463,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1483,7 +1487,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1491,7 +1495,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + gcd @@ -1501,7 +1505,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + gcd @@ -1524,7 +1528,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1546,7 +1550,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1574,7 +1578,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1594,7 +1598,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1616,7 +1620,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1644,7 +1648,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1664,7 +1668,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1685,7 +1689,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1713,7 +1717,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1728,7 +1732,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1736,7 +1740,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ¬ @@ -1749,14 +1753,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + for all @@ -1783,14 +1787,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + @@ -1820,7 +1824,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1831,7 +1835,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1845,7 +1849,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1855,7 +1859,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ̲ @@ -1865,7 +1869,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1873,7 +1877,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1882,7 +1886,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1891,7 +1895,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1913,7 +1917,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> | m:geq | m:leq | m:equivalent]"> - + @@ -1925,7 +1929,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1934,7 +1938,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1943,7 +1947,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1952,7 +1956,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1961,7 +1965,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1970,7 +1974,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1979,7 +1983,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -1988,7 +1992,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2000,7 +2004,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - @@ -2009,7 +2013,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + + @@ -2023,7 +2027,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2032,7 +2036,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2041,7 +2045,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2050,7 +2054,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2059,7 +2063,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2068,7 +2072,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2077,7 +2081,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2086,7 +2090,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2105,7 +2109,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2115,7 +2119,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ln @@ -2126,7 +2130,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + ln @@ -2142,7 +2146,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2153,7 +2157,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + log @@ -2165,7 +2169,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + log @@ -2183,7 +2187,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + log @@ -2209,7 +2213,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2217,7 +2221,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2238,7 +2242,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2256,7 +2260,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2265,7 +2269,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2286,7 +2290,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2310,7 +2314,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2318,7 +2322,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2327,7 +2331,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2336,7 +2340,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2359,14 +2363,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + @@ -2383,7 +2387,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2421,7 +2425,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> and $PARAM=$PAR_SAME"> - + @@ -2444,7 +2448,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2472,7 +2476,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2493,7 +2497,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2516,7 +2520,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2544,7 +2548,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2566,7 +2570,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> and $PARAM=$PAR_SAME"> - + @@ -2589,7 +2593,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2616,7 +2620,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + \ @@ -2631,7 +2635,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2647,7 +2651,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2658,7 +2662,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2667,7 +2671,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2689,7 +2693,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2698,7 +2702,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2716,7 +2720,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2724,7 +2728,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + lim @@ -2754,7 +2758,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> self::m:arctan]]"> - + @@ -2778,7 +2782,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2838,7 +2842,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2851,14 +2855,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + σ @@ -2873,14 +2877,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + σ @@ -2898,14 +2902,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + median @@ -2920,14 +2924,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + mode @@ -2942,7 +2946,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2966,7 +2970,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2983,7 +2987,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -2996,7 +3000,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -3011,14 +3015,14 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + - + det @@ -3029,7 +3033,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -3037,7 +3041,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + T @@ -3067,7 +3071,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> m:scalarproduct[1] | m:outerproduct[1]]"> - + @@ -3076,7 +3080,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - + @@ -3085,7 +3089,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements --> - +