From: Irene Schena Date: Wed, 6 Mar 2002 11:27:12 +0000 (+0000) Subject: Modified Files: X-Git-Tag: V_0_3_0_debian_8~245 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0f057b69d304a8ca6e6d1e4b67f00755d1650636;p=helm.git Modified Files: 1) link.xsl mmlctop.xsl-0.14 mmlextension.xsl mmlnotation.xsl: removed redundant namespace prefix m: of the MML xref attribute --- diff --git a/helm/style/link.xsl b/helm/style/link.xsl index 48bb02b66..e3568a18f 100644 --- a/helm/style/link.xsl +++ b/helm/style/link.xsl @@ -48,8 +48,8 @@ xlink:href) --> - - + + diff --git a/helm/style/mmlctop.xsl-0.14 b/helm/style/mmlctop.xsl-0.14 index be41c5be3..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 --> - + diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl index 7e9bd1e5f..b9cd3165e 100644 --- a/helm/style/mmlextension.xsl +++ b/helm/style/mmlextension.xsl @@ -414,7 +414,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1715,7 +1715,7 @@ which generates the toplevel element (see for instance xlink) --> - + ] @@ -1725,7 +1725,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1740,7 +1740,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1757,7 +1757,7 @@ which generates the toplevel element (see for instance xlink) --> - + β @@ -1769,7 +1769,7 @@ which generates the toplevel element (see for instance xlink) --> - + β * @@ -1782,7 +1782,7 @@ which generates the toplevel element (see for instance xlink) --> - + β @@ -1794,7 +1794,7 @@ which generates the toplevel element (see for instance xlink) --> - + β * @@ -1805,7 +1805,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1815,7 +1815,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1823,7 +1823,7 @@ which generates the toplevel element (see for instance xlink) --> - + @@ -1898,7 +1898,7 @@ which generates the toplevel element (see for instance xlink) --> - + diff --git a/helm/style/mmlnotation.xsl b/helm/style/mmlnotation.xsl index a89a2e4b9..3ebf23ba7 100644 --- a/helm/style/mmlnotation.xsl +++ b/helm/style/mmlnotation.xsl @@ -53,7 +53,7 @@ - + @@ -72,7 +72,7 @@ __ - + = @@ -151,7 +151,7 @@ - + @@ -170,7 +170,7 @@ __ - + @@ -199,7 +199,7 @@ - + @@ -218,7 +218,7 @@ - + { @@ -240,7 +240,7 @@ - + } @@ -256,7 +256,7 @@ - + { @@ -285,7 +285,7 @@ - + } @@ -307,7 +307,7 @@ - +