]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/mmlctop.xsl-0.14
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
----------------------------------------------------------------------
[helm.git] / helm / style / mmlctop.xsl-0.14
diff --git a/helm/style/mmlctop.xsl-0.14 b/helm/style/mmlctop.xsl-0.14
index aca072bb645556ccdaea01b5fde52bf5196ec2e3..4ab889155b1293fd5cfab544a816643e7889c290 100755 (executable)
--- a/helm/style/mmlctop.xsl-0.14
+++ b/helm/style/mmlctop.xsl-0.14
@@ -20,6 +20,7 @@
 <!--  Added the namespace prefix to all the xref attributes -->
 <!--  Changed the mml prefix into m                         -->
 <!--  Added m:xref to every mo element                      -->
+<!--  Changed mchar into the corresponding entity           -->
 <!--  First draft: April 27 2001, Irene Schena              -->
 <!-- ====================================================== -->
 
@@ -357,7 +358,7 @@ LINEAR ALGEBRA
           <m:mo>+</m:mo>
           <m:mn> <xsl:value-of select="text()[2]"/> </m:mn>
         </xsl:if>
-        <m:mo> <m:mchar name="InvisibleTimes"/> </m:mo>
+        <m:mo>&#x02062;</m:mo>
         <m:mo>i</m:mo>
       </m:mfenced>
     </xsl:when>
@@ -373,7 +374,7 @@ LINEAR ALGEBRA
             <m:mo>+</m:mo>
             <m:mn> <xsl:apply-templates select="text()[2]"/> </m:mn>
           </xsl:if>
-          <m:mo> <m:mchar name="InvisibleTimes"/> </m:mo>
+          <m:mo>&#x02062;</m:mo>
           <m:mo>i</m:mo>
         </m:mfenced>
         <m:mn> <xsl:value-of select="@base"/> </m:mn>
@@ -399,7 +400,7 @@ LINEAR ALGEBRA
     <xsl:when test="@type='polar' and not(@base) and child::m:sep[1]">
       <m:mrow>
         <m:mo>Polar</m:mo>
-        <m:mo> <m:mchar name="InvisibleTimes"/> </m:mo>
+        <m:mo>&#x02062;</m:mo>
         <m:mfenced separators=",">
           <m:mn> <xsl:apply-templates select="text()[1]"/> </m:mn>
           <m:mn> <xsl:apply-templates select="text()[2]"/> </m:mn>
@@ -410,7 +411,7 @@ LINEAR ALGEBRA
       <m:msub>
         <m:mrow>
           <m:mo>Polar</m:mo>
-          <m:mo> <m:mchar name="InvisibleTimes"/> </m:mo>
+          <m:mo>&#x02062;</m:mo>
           <m:mfenced separators=",">
             <m:mn> <xsl:apply-templates select="text()[1]"/> </m:mn>
             <m:mn> <xsl:apply-templates select="text()[2]"/> </m:mn>
@@ -444,7 +445,7 @@ LINEAR ALGEBRA
           <m:mo>+</m:mo>
           <m:mn> <xsl:value-of select="text()[2]"/> </m:mn>
         </xsl:if>
-        <m:mo> <m:mchar name="InvisibleTimes"/> </m:mo>
+        <m:mo>&#x02062;</m:mo>
         <m:mo>i</m:mo>
       </m:mfenced>
     </xsl:when>
@@ -460,7 +461,7 @@ LINEAR ALGEBRA
             <m:mo>+</m:mo>
             <m:mn> <xsl:apply-templates select="text()[2]"/> </m:mn>
           </xsl:if>
-          <m:mo> <m:mchar name="InvisibleTimes"/> </m:mo>
+          <m:mo>&#x02062;</m:mo>
           <m:mo>i</m:mo>
         </m:mfenced>
         <m:mn> <xsl:value-of select="@base"/> </m:mn>
@@ -486,7 +487,7 @@ LINEAR ALGEBRA
     <xsl:when test="@type='polar' and not(@base) and child::m:sep[1]">
       <m:mrow m:xref="{@id}">
         <m:mo>Polar</m:mo>
-        <m:mo> <m:mchar name="InvisibleTimes"/> </m:mo>
+        <m:mo>&#x02062;</m:mo>
         <m:mfenced separators=",">
           <m:mn> <xsl:apply-templates select="text()[1]"/> </m:mn>
           <m:mn> <xsl:apply-templates select="text()[2]"/> </m:mn>
@@ -497,7 +498,7 @@ LINEAR ALGEBRA
       <m:msub m:xref="{@id}">
         <m:mrow>
           <m:mo>Polar</m:mo>
-          <m:mo> <m:mchar name="InvisibleTimes"/> </m:mo>
+          <m:mo>&#x02062;</m:mo>
           <m:mfenced separators=",">
             <m:mn> <xsl:apply-templates select="text()[1]"/> </m:mn>
             <m:mn> <xsl:apply-templates select="text()[2]"/> </m:mn>
@@ -649,8 +650,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="m:fn/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name='ApplyFunction'/> </m:mo>
+        </xsl:if>&#x02061;</m:mo>
     <m:mfenced separators=",">
       <xsl:apply-templates select = "*[position()>1]" mode = "semantics"/>
     </m:mfenced>
@@ -688,7 +688,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
       </xsl:attribute>
     </xsl:if>
     <xsl:apply-templates select = "*[1]" mode = "semantics"/>
-    <m:mo> <m:mchar name='ApplyFunction'/> </m:mo>
+    <m:mo>&#x02061;</m:mo>
     <m:mfenced separators=",">
       <xsl:apply-templates select = "*[position()>1]" mode = "semantics"/>
     </m:mfenced>
@@ -819,8 +819,8 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
         <xsl:value-of select="@id"/>
       </xsl:attribute>
     </xsl:if>
-    <m:mo> <m:mchar name='Lambda'/> </m:mo>
-    <m:mo> <m:mchar name='ApplyFunction'/> </m:mo>
+    <m:mo>&#x0039B;</m:mo>
+    <m:mo>&#x02061;</m:mo>
     <m:mfenced separators=",">
       <xsl:for-each select = "*">
         <xsl:choose>
@@ -846,7 +846,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
       </xsl:attribute>
     </xsl:if>
     <xsl:apply-templates select = "*[1]" mode = "semantics"/>
-    <m:mo> <m:mchar name='ApplyFunction'/> </m:mo>
+    <m:mo>&#x02061;</m:mo>
     <m:mfenced separators=",">
       <xsl:apply-templates select = "*[position()>1]" mode = "semantics"/>
     </m:mfenced>
@@ -870,8 +870,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="../m:compose/@id"/>
           </xsl:attribute>
-        </xsl:if>
-      <m:mchar name="SmallCircle"/> </m:mo>
+        </xsl:if>&#x02218;</m:mo>
       <xsl:apply-templates select = "." mode="semantics"/>
     </xsl:for-each>
   </m:mfenced>
@@ -898,9 +897,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
         <xsl:value-of select="@id"/>
       </xsl:attribute>
     </xsl:if>
-    <m:mo form="prefix" fence="true" stretchy="true" lspace="0em" rspace="0em">
-      <m:mchar name="LeftFloor"/>
-    </m:mo>
+    <m:mo form="prefix" fence="true" stretchy="true" lspace="0em" rspace="0em">&#x0230A;</m:mo>
     <m:mfrac>
 <!-- HELM: added -->        
         <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
@@ -920,9 +917,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
         </xsl:apply-templates>
       </m:mrow>
     </m:mfrac>
-    <m:mo form="postfix" fence="true" stretchy="true" lspace="0em" rspace="0em">
-      <m:mchar name="LeftFloor"/>
-    </m:mo>
+    <m:mo form="postfix" fence="true" stretchy="true" lspace="0em" rspace="0em">&#x0230A;</m:mo>
   </m:mrow>
 </xsl:template>
 
@@ -1398,7 +1393,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
   <xsl:if test="*[3]">
     <xsl:for-each select = "*[position()>2]">
 <!-- HELM: to distinguish between * and the application -->
-<!--      <m:mo> <mchar name="InvisibleTimes"/> </m:mo> -->
+<!--      <m:mo>&#x02062;</m:mo> -->
       <m:mo>
 <!-- HELM: added -->        
         <xsl:if test="($SEM_SW=$SEM_XREF or $SEM_SW=$SEM_XREF_EXT) and @id">
@@ -1536,8 +1531,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="../m:and/@id"/>
           </xsl:attribute>
-        </xsl:if>
- <m:mchar name="wedge"/></m:mo>
+        </xsl:if>&#x02227;</m:mo>
     <xsl:apply-templates select="." mode = "semantics">
       <xsl:with-param name="IN_PREC" select="$AND_PREC"/>
       <xsl:with-param name="PAREN" select="$PAREN"/>
@@ -1607,8 +1601,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="../m:or/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name="vee"/> </m:mo>
+        </xsl:if>&#x02228;</m:mo>
     <xsl:apply-templates select="." mode = "semantics">
       <xsl:with-param name="IN_PREC" select="$OR_PREC"/>
       <xsl:with-param name="PAREN" select="$PAREN"/>
@@ -1677,8 +1670,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="../m:xor/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name="xor"/> </m:mo>
+        </xsl:if>&#x022BB;</m:mo>
     <xsl:apply-templates select="." mode = "semantics">
       <xsl:with-param name="IN_PREC" select="$XOR_PREC"/>
       <xsl:with-param name="PAREN" select="$PAREN"/>
@@ -1701,7 +1693,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="m:not/@id"/>
           </xsl:attribute>
-        </xsl:if><m:mchar name="not"/></m:mo>
+        </xsl:if>&#x000AC;</m:mo>
     <xsl:apply-templates select = "*[2]" mode = "semantics">
       <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
     </xsl:apply-templates>
@@ -1755,8 +1747,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="m:exists/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name="Exists"/> </m:mo>
+        </xsl:if>&#x02203;</m:mo>
     <xsl:if test="count(m:bvar) &gt; 1">
       <m:mfenced separators=",">
         <xsl:for-each select = "m:bvar">
@@ -1821,8 +1812,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="m:conjugate/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name="UnderBar"/> </m:mo>
+        </xsl:if>&#x00332;</m:mo>
   </m:mover>
 </xsl:template>
 
@@ -1893,7 +1883,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:neq/@id"/>
           </xsl:attribute>
         </xsl:if>
-          <m:mchar name="NotEqual"/>
+        &#x02260;
         </xsl:if>
         <xsl:if test="*[1]=m:approx">
 <!-- HELM: added -->        
@@ -1902,7 +1892,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:approx/@id"/>
           </xsl:attribute>
         </xsl:if>
-          <m:mchar name="approxeq"/>
+        &#x0224A;
         </xsl:if>
         <xsl:if test="*[1]=m:tendsto">
 <!-- HELM: added -->        
@@ -1911,7 +1901,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:tendsto/@id"/>
           </xsl:attribute>
         </xsl:if>
-          <m:mchar name="RightArrow"/>
+        &#x02192;
         </xsl:if>
         <xsl:if test="*[1]=m:implies">
 <!-- HELM: added -->        
@@ -1920,7 +1910,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:implies/@id"/>
           </xsl:attribute>
         </xsl:if>
-          <m:mchar name="DoubleRightArrow"/>
+        &#x021D2;
         </xsl:if>
         <xsl:if test="*[1]=m:in">
 <!-- HELM: added -->        
@@ -1929,7 +1919,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:in/@id"/>
           </xsl:attribute>
         </xsl:if>
-          <m:mchar name="Element"/>
+        &#x02208;
         </xsl:if>
         <xsl:if test="*[1]=m:notin">
 <!-- HELM: added -->        
@@ -1938,7 +1928,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:notin/@id"/>
           </xsl:attribute>
         </xsl:if>
-          <m:mchar name="NotElement"/>
+        &#x02209;
         </xsl:if>
         <xsl:if test="*[1]=m:notsubset">
 <!-- HELM: added -->        
@@ -1947,7 +1937,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:notsubset/@id"/>
           </xsl:attribute>
         </xsl:if>
-          <m:mchar name="NotSubset"/>
+        &#x02284;
         </xsl:if>
         <xsl:if test="*[1]=m:notprsubset">
 <!-- HELM: added -->        
@@ -1956,7 +1946,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:notprsubset/@id"/>
           </xsl:attribute>
         </xsl:if>
-          <m:mchar name="NotSubsetEqual"/>
+        &#x02288;
         </xsl:if>
       </m:mo>
       <xsl:apply-templates select = "*[3]" mode = "semantics"/>
@@ -1991,7 +1981,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="../m:subset/@id"/>
           </xsl:attribute>
         </xsl:if>
-            <m:mchar name="SubsetEqual"/>
+        &#x02286;
           </xsl:if>
           <xsl:if test="../*[self::m:prsubset][1]">
 <!-- HELM: added -->        
@@ -2000,7 +1990,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="../m:prsubset/@id"/>
           </xsl:attribute>
         </xsl:if>
-            <m:mchar name="subset"/>
+        &#x02282;
           </xsl:if>
           <xsl:if test="../*[self::m:eq][1]">
 <!-- HELM: added -->        
@@ -2036,7 +2026,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="../m:geq/@id"/>
           </xsl:attribute>
         </xsl:if>
-            <m:mchar name="geq"/>
+        &#x02265;
           </xsl:if>
           <xsl:if test="../*[self::m:leq][1]">
 <!-- HELM: added -->        
@@ -2045,7 +2035,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="../m:leq/@id"/>
           </xsl:attribute>
         </xsl:if>
-            <m:mchar name="leq"/>
+        &#x02264;
           </xsl:if>
           <xsl:if test="../*[self::m:equivalent][1]">
 <!-- HELM: added -->        
@@ -2054,7 +2044,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="../m:equivalent/@id"/>
           </xsl:attribute>
         </xsl:if>
-            <m:mchar name="Congruent"/>
+        &#x02261;
           </xsl:if>
         </m:mo>
         <xsl:apply-templates select = "." mode="semantics"/>
@@ -2096,7 +2086,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
         </xsl:if>ln</m:mo>
       </xsl:otherwise>
     </xsl:choose>
-    <m:mo> <m:mchar name='ApplyFunction'/> </m:mo>
+    <m:mo>&#x02061;</m:mo>
     <xsl:apply-templates select = "*[2]" mode = "semantics">
       <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
     </xsl:apply-templates>
@@ -2156,7 +2146,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
         </xsl:if>
       </xsl:otherwise>
     </xsl:choose>
-    <m:mo> <m:mchar name='ApplyFunction'/> </m:mo>
+    <m:mo>&#x02061;</m:mo>
     <xsl:if test="*[2]=m:logbase">
       <xsl:apply-templates select = "*[3]" mode = "semantics">
         <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
@@ -2334,7 +2324,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:laplacian/@id"/>
           </xsl:attribute>
         </xsl:if>
-      <m:mo> <m:mchar name="Delta"/> </m:mo>
+      <m:mo>&#x00394;</m:mo>
       <m:mn>2</m:mn>
     </m:msup>
     <xsl:apply-templates select = "*[2]" mode = "semantics"/>
@@ -2439,8 +2429,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="../m:union/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name="Union"/> </m:mo>
+        </xsl:if>&#x022C3;</m:mo>
     <xsl:apply-templates select = "." mode="semantics">
       <xsl:with-param name="IN_PREC" select="$UNION_PREC"/>
       <xsl:with-param name="PAREN" select="$PAREN"/>
@@ -2512,8 +2501,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="../m:intersect/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name="Intersection"/> </m:mo>
+        </xsl:if>&#x022C2;</m:mo>
     <xsl:apply-templates select = "." mode="semantics">
       <xsl:with-param name="IN_PREC" select="$INTERSECT_PREC"/>
       <xsl:with-param name="PAREN" select="$PAREN"/>
@@ -2628,7 +2616,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:sum/@id"/>
           </xsl:attribute>
         </xsl:if>
-              <m:mchar name="Sum"/>
+        &#x02211;
             </xsl:if>
             <xsl:if test="*[1]=m:product">
 <!-- HELM: added -->        
@@ -2637,7 +2625,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:product/@id"/>
           </xsl:attribute>
         </xsl:if>
-              <m:mchar name="Product"/>
+        &#x0220F;
             </xsl:if>
           </m:mo>
           <m:mrow>
@@ -2659,7 +2647,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:sum/@id"/>
           </xsl:attribute>
         </xsl:if>
-              <m:mchar name="Sum"/>
+        &#x02211;
             </xsl:if>
             <xsl:if test="*[1]=m:product">
 <!-- HELM: added -->        
@@ -2668,7 +2656,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:product/@id"/>
           </xsl:attribute>
         </xsl:if>
-              <m:mchar name="Product"/>
+        &#x0220F;
             </xsl:if>
           </m:mo>
           <xsl:apply-templates select = "*[3]" mode = "semantics"/>
@@ -2697,7 +2685,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
       <m:mrow>
         <xsl:if test="*[2]=m:bvar and *[3]=m:lowlimit">
             <xsl:apply-templates select = "*[2]" mode = "semantics"/>
-            <m:mo> <m:mchar name="RightArrow"/> </m:mo>
+            <m:mo>&#x02192;</m:mo>
             <xsl:apply-templates select = "*[3]" mode = "semantics"/>
         </xsl:if>
         <xsl:if test="*[2]=m:bvar and *[3]=m:condition">
@@ -2733,7 +2721,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
         <xsl:apply-templates select = "../*[3]" mode = "semantics"/>
       </m:msup>
     </xsl:if>
-    <m:mo> <m:mchar name='ApplyFunction'/> </m:mo>
+    <m:mo>&#x02061;</m:mo>
     <xsl:apply-templates select = "*[2]" mode = "semantics">
       <xsl:with-param name="IN_PREC" select="$FUNCTION_PREC"/>
       <xsl:with-param name="PAR_NO_IGNORE" select="$NO"/>
@@ -2827,8 +2815,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="m:sdev/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name="sigma"/> </m:mo>
+        </xsl:if>&#x003C3;</m:mo>
     <m:mfenced separators=",">
       <xsl:for-each select = "*[position()>1]">
         <xsl:apply-templates select = "." mode="semantics"/>
@@ -2850,8 +2837,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
           <xsl:attribute name="m:xref">
             <xsl:value-of select="m:variance/@id"/>
           </xsl:attribute>
-        </xsl:if>
-    <m:mchar name="sigma"/> </m:mo>
+        </xsl:if>&#x003C3;</m:mo>
     <m:msup>
       <m:mfenced separators=",">
         <xsl:for-each select = "*[position()>1]">
@@ -3048,7 +3034,7 @@ an mo. Mixed content: mrow which contains mo + presentation elements -->
             <xsl:value-of select="m:vectorproduct/@id"/>
           </xsl:attribute>
         </xsl:if>
-        <m:mchar name="Cross"/>
+        &#x02A2F;
       </xsl:if>
       <xsl:if test="m:scalarproduct[1] | m:outerproduct[1]">
 <!-- HELM: added -->        
Unnamed repository; edit this file 'description' to name the repository.