From: Irene Schena <irene.schena@unibo.it>
Date: Tue, 24 Jul 2001 16:12:47 +0000 (+0000)
Subject: ----------------------------------------------------------------------
X-Git-Tag: v0_1_3~104
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5d9c64e007c6eff9447b2ef67d2a680c86c2775d;p=helm.git

----------------------------------------------------------------------
Modified Files:
1) mmlctop.xsl-0.14, mmlextension.xsl: changed mchar into entities and
formatted new proof elements.
----------------------------------------------------------------------
---

diff --git a/helm/style/arith.xsl b/helm/style/arith.xsl
index d06a0f252..6393d2722 100644
--- a/helm/style/arith.xsl
+++ b/helm/style/arith.xsl
@@ -184,14 +184,3 @@
 </xsl:template>
 
 </xsl:stylesheet>
-
-
-
-
-
-
-
-
-
-
-
diff --git a/helm/style/basic.xsl b/helm/style/basic.xsl
index a6150ff40..6a1972c53 100644
--- a/helm/style/basic.xsl
+++ b/helm/style/basic.xsl
@@ -238,8 +238,3 @@ and (count(child::*) = 2) and APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Logic_T
 <!-- see arith.xsl --> <!-- FG -->
 
 </xsl:stylesheet>
-
-
-
-
-
diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index 241491a98..697624810 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -270,8 +270,3 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
 </xsl:template>
 
 </xsl:stylesheet>
-
-
-
-
-
diff --git a/helm/style/contentlib.xsl b/helm/style/contentlib.xsl
index e1905c8b9..65e08c683 100644
--- a/helm/style/contentlib.xsl
+++ b/helm/style/contentlib.xsl
@@ -109,4 +109,3 @@
 </xsl:template>
 
 </xsl:stylesheet>
-
diff --git a/helm/style/drop_coercions.xsl b/helm/style/drop_coercions.xsl
index 688d3974b..a259955dd 100644
--- a/helm/style/drop_coercions.xsl
+++ b/helm/style/drop_coercions.xsl
@@ -128,7 +128,3 @@
 
 
 </xsl:stylesheet>
-
-
-
-
diff --git a/helm/style/genmmlid.xsl b/helm/style/genmmlid.xsl
index fb636046f..b11ff7eb9 100644
--- a/helm/style/genmmlid.xsl
+++ b/helm/style/genmmlid.xsl
@@ -53,6 +53,3 @@
 </xsl:template>
 
 </xsl:stylesheet> 
-
-
-
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index 93791685c..a6a840a57 100644
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -393,5 +393,3 @@
 </xsl:template> 
 
 </xsl:stylesheet> 
-
-
diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl
index 5c7052c03..e8f82e7b2 100644
--- a/helm/style/html_set.xsl
+++ b/helm/style/html_set.xsl
@@ -373,10 +373,3 @@
 </xsl:template> 
 
 </xsl:stylesheet> 
-
-
-
-
-
-
-
diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index f9b535f1e..ae225272d 100644
--- a/helm/style/inductive.xsl
+++ b/helm/style/inductive.xsl
@@ -403,6 +403,4 @@
  </xsl:choose>
 </xsl:template>
 
-
 </xsl:stylesheet>
-
diff --git a/helm/style/lambda.xsl b/helm/style/lambda.xsl
index 5dfb30a99..28c876fa0 100644
--- a/helm/style/lambda.xsl
+++ b/helm/style/lambda.xsl
@@ -156,5 +156,3 @@
 </xsl:template>
 
 </xsl:stylesheet>
-
-
diff --git a/helm/style/link.xsl b/helm/style/link.xsl
index ba22dea12..48bb02b66 100644
--- a/helm/style/link.xsl
+++ b/helm/style/link.xsl
@@ -116,4 +116,3 @@ xlink:href) -->
 </xsl:template>
 
 </xsl:stylesheet> 
-
diff --git a/helm/style/links_library.xsl b/helm/style/links_library.xsl
index 0f6613c28..5611e3a75 100644
--- a/helm/style/links_library.xsl
+++ b/helm/style/links_library.xsl
@@ -358,6 +358,3 @@
 </xsl:template>
 
 </xsl:stylesheet> 
-
-
-
diff --git a/helm/style/mk_meta_theory.xsl b/helm/style/mk_meta_theory.xsl
index bdae203af..34d6b1ccd 100644
--- a/helm/style/mk_meta_theory.xsl
+++ b/helm/style/mk_meta_theory.xsl
@@ -203,16 +203,3 @@
 
 
 </xsl:stylesheet>
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/helm/style/mmlctop.xsl-0.14 b/helm/style/mmlctop.xsl-0.14
index aca072bb6..4ab889155 100755
--- 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 -->        
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index bb13c876e..6572c0556 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -373,21 +373,27 @@ which generates the toplevel element (see for instance xlink) -->
      <m:mtable align="baseline 1" equalrows="false" columnalign="left">
       <m:mtr>
        <m:mtd>
-        <xsl:apply-templates select="m:ci"/>
-        <m:mo>:</m:mo>
+        <m:mrow>
+         <xsl:apply-templates select="m:ci"/>
+         <m:mo>:</m:mo>
+        </m:mrow>
        </m:mtd>
       </m:mtr>
       <m:mtr>
        <m:mtd>
+        <m:mrow>
          <xsl:apply-templates select="m:type"/>
+        </m:mrow>
        </m:mtd>
       </m:mtr>
      </m:mtable>
     </xsl:when>
     <xsl:otherwise>
-     <xsl:apply-templates select="m:ci"/>
-     <m:mo>:</m:mo>
-     <xsl:apply-templates select="m:type"/>
+     <m:mrow>
+      <xsl:apply-templates select="m:ci"/>
+      <m:mo>:</m:mo>
+      <xsl:apply-templates select="m:type"/>
+     </m:mrow>
     </xsl:otherwise>
    </xsl:choose>
   </xsl:when>
@@ -417,7 +423,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
+            <m:mo mathcolor="Blue">&#8704;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
            </m:mrow>
           </m:mtd>
@@ -433,7 +439,7 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
+        <m:mo mathcolor="Blue">&#8704;</m:mo>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <m:mo>:</m:mo>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -985,17 +991,21 @@ which generates the toplevel element (see for instance xlink) -->
         <!-- CSC: next if until the annotationHelper can handle mactions -->
         <xsl:if test="not($explodeall)">
          <!-- Details hided (default) -->
-         <m:mrow>
-          <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</m:mtext>
-          <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-          <xsl:apply-templates select="*[position()=3]"/>
-          <m:mrow>
-           <m:mphantom>
-            <m:mtext>_</m:mtext>
-           </m:mphantom>
-           <m:mtext mathcolor="Green">(explain)</m:mtext>
-          </m:mrow>
-         </m:mrow>
+         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+          <m:mtr>
+           <m:mtd>
+            <m:mrow>
+             <m:mtext mathcolor="Maroon">We&#x00a0;can&#x00a0;prove</m:mtext>
+             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+             <xsl:apply-templates select="*[position()=3]"/>
+             <m:mrow>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <m:mtext mathcolor="Green">(explain)</m:mtext>
+             </m:mrow>
+            </m:mrow>
+           </m:mtd>
+          </m:mtr>
+         </m:mtable>
         </xsl:if>
         <!-- Show details -->
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1009,7 +1019,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext mathcolor="Maroon">we&#x00a0;proved </m:mtext>
+            <m:mtext mathcolor="Maroon">we&#x00a0;proved</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()=3]"/>
             <m:mrow>
@@ -1043,15 +1053,12 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
-
-      <!-- CSC: Il caso che segue e' stato buttato li' giusto per vedere -->
-      <!-- qualche cosa. Irene, appena puoi, risistemalo.                -->
       <xsl:when test="$name='by_induction'">
        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mtext mathcolor="red">We prove </m:mtext>
+           <m:mtext mathcolor="red">We&#x00a0;prove</m:mtext>
            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <xsl:apply-templates select="../*[3]"/>
           </m:mrow>
@@ -1060,9 +1067,9 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mtext mathcolor="red">by induction on </m:mtext>
+           <m:mtext mathcolor="red">by&#x00a0;induction&#x00a0;on</m:mtext>
            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-           <xsl:apply-templates
+           <xsl:apply-templates 
             select="*[position()=last()]/*[position()=last()]"/>
           </m:mrow>
          </m:mtd>
@@ -1070,12 +1077,13 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <m:mtable align="baseline 1" equalrows="false" columnalign="left">
             <xsl:for-each select="*[position()>3 and not(position()=last())]">
              <m:mtr>
               <m:mtd>
-               <xsl:apply-templates select="."/>
+               <m:mrow>
+                <xsl:apply-templates select="."/>
+               </m:mrow>
               </m:mtd>
              </m:mtr>
             </xsl:for-each>
@@ -1091,7 +1099,7 @@ which generates the toplevel element (see for instance xlink) -->
         <m:mtr>
          <m:mtd>
           <m:mrow>
-           <m:mtext mathcolor="red">Case </m:mtext>
+           <m:mtext mathcolor="red">Case</m:mtext>
            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <xsl:apply-templates select="*[2]"/>
           </m:mrow>
@@ -1105,7 +1113,9 @@ which generates the toplevel element (see for instance xlink) -->
             <xsl:if test="*[3]/*[position()>1]">
              <m:mtr>
               <m:mtd>
-               <m:mtext mathcolor="red">By induction hypothesis, we have:</m:mtext>
+               <m:mrow>
+                <m:mtext mathcolor="red">By&#x00a0;induction&#x00a0;hypothesis,&#x00a0;we&#x00a0;have:</m:mtext>
+               </m:mrow>
               </m:mtd>
              </m:mtr>
              <m:mtr>
@@ -1125,7 +1135,9 @@ which generates the toplevel element (see for instance xlink) -->
             </xsl:if>
             <m:mtr>
              <m:mtd>
-              <xsl:apply-templates select="*[4]"/>
+              <m:mrow>
+               <xsl:apply-templates select="*[4]"/>
+              </m:mrow>
              </m:mtd>
             </m:mtr>
            </m:mtable>
@@ -1155,6 +1167,7 @@ which generates the toplevel element (see for instance xlink) -->
         </xsl:choose>
        </m:mrow>
       </xsl:when>
+      <!-- false_ind  -->
       <xsl:when test="$name='false_ind'">
        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
@@ -1173,8 +1186,6 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtr>
        </m:mtable>
       </xsl:when>
-      <!--CSC fine della parte da risistemare -->
-
       <!-- LET-IN -->
       <xsl:when test="$name='letin'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1278,7 +1289,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>Then apply it to</m:mtext>
+            <m:mtext>Then&#x00a0;apply&#x00a0;it&#x00a0;to</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()>2]"/>
            </m:mrow>
@@ -1308,7 +1319,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>In particular, we have</m:mtext>
+            <m:mtext>In&#x00a0;particular,&#x00a0;we&#x00a0;have</m:mtext>
            </m:mrow>
           </m:mtd>
          </m:mtr>
@@ -1343,8 +1354,6 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
-      <!-- CSC: Il caso che segue e' stato buttato li' giusto per vedere -->
-      <!-- qualche cosa. Irene, appena puoi, risistemalo.                -->
       <!-- full_or_ind -->
       <xsl:when test="$name='full_or_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1367,7 +1376,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>We proceed by cases to prove</m:mtext>
+            <m:mtext>We&#x00a0;proceed&#x00a0;by&#x00a0;cases&#x00a0;to&#x00a0;prove</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[3]"/>
            </m:mrow>
@@ -1376,7 +1385,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>Left: suppose</m:mtext>
+            <m:mtext>Left:&#x00a0;suppose</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <m:mo stretchy="false">(</m:mo>
             <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
@@ -1388,8 +1397,8 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
          <m:mtr>
           <m:mtd>
-           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <m:mrow>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[4]/*[3]"/>
            </m:mrow>
           </m:mtd>
@@ -1397,7 +1406,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>Right: suppose</m:mtext>
+            <m:mtext>Right:&#x00a0;suppose</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <m:mo stretchy="false">(</m:mo>
             <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
@@ -1416,7 +1425,6 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
-      <!--CSC fine della parte da risistemare -->
       <!-- OR_IND -->
       <xsl:when test="$name='or_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1439,11 +1447,11 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>We prove</m:mtext>
+            <m:mtext>We&#x00a0;prove</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[3]"/>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <m:mtext>by cases:</m:mtext>
+            <m:mtext>by&#x00a0;cases:</m:mtext>
            </m:mrow>
           </m:mtd>
          </m:mtr>
@@ -1493,7 +1501,7 @@ which generates the toplevel element (see for instance xlink) -->
             <m:mtext>:</m:mtext>
             <xsl:apply-templates select="*[4]"/>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <m:mtext>such that</m:mtext>
+            <m:mtext>such&#x00a0;that</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <m:mtext>(</m:mtext>
              <xsl:apply-templates select="*[5]"/>
@@ -1545,7 +1553,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext mathcolor="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1563,7 +1571,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext mathcolor="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Maroon">we&#x00a0;get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1673,43 +1681,43 @@ which generates the toplevel element (see for instance xlink) -->
  <xsl:variable name="symbol">
   <xsl:choose>
    <xsl:when test="m:and[1]">
-    <xsl:value-of select="'wedge'"/>
+    <xsl:value-of select="'&#8743;'"/>
    </xsl:when>
    <xsl:when test="m:or[1]">
-    <xsl:value-of select="'vee'"/>
+    <xsl:value-of select="'&#8744;'"/>
    </xsl:when>
    <xsl:when test="m:geq[1]">
-    <xsl:value-of select="'geq'"/>
+    <xsl:value-of select="'&#8805;'"/>
    </xsl:when>
    <xsl:when test="m:leq[1]">
-    <xsl:value-of select="'leq'"/>
+    <xsl:value-of select="'&#8804;'"/>
    </xsl:when>
    <xsl:when test="m:gt[1]">
-    <xsl:value-of select="'gt'"/>
+    <xsl:value-of select="'&#62;'"/>
    </xsl:when>
    <xsl:when test="m:lt[1]">
-    <xsl:value-of select="'lt'"/>
+    <xsl:value-of select="'&#60;&#32;'"/>
    </xsl:when>
    <xsl:when test="m:eq[1]">
-    <xsl:value-of select="'Equal'"/>
+    <xsl:value-of select="'&#61;'"/>
    </xsl:when>
    <xsl:when test="m:in[1]">
-    <xsl:value-of select="'Element'"/>
+    <xsl:value-of select="'&#x02208;'"/>
    </xsl:when>
    <xsl:when test="m:subset[1]">
-    <xsl:value-of select="'SubsetEqual'"/>
+    <xsl:value-of select="'&#x02286;'"/>
    </xsl:when>
    <xsl:when test="m:prsubset[1]">
-    <xsl:value-of select="'subset'"/>
+    <xsl:value-of select="'&#x02282;'"/>
    </xsl:when>
    <xsl:when test="m:intersect[1]">
-    <xsl:value-of select="'Intersection'"/>
+    <xsl:value-of select="'&#x022C2;'"/>
    </xsl:when>
    <xsl:when test="m:union[1]">
-    <xsl:value-of select="'Union'"/>
+    <xsl:value-of select="'&#x022C3;'"/>
    </xsl:when>
    <xsl:when test="m:setdiff[1]">
-    <xsl:value-of select="'Backslash'"/>
+    <xsl:value-of select="'&#x02216;'"/>
    </xsl:when>
   </xsl:choose>
  </xsl:variable>
@@ -1737,9 +1745,7 @@ which generates the toplevel element (see for instance xlink) -->
       <m:mtd>
        <m:mrow>
         <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-        <m:mo m:xref="{*[1]/@id}"> 
-         <m:mchar name="{$symbol}"/>
-        </m:mo>
+        <m:mo m:xref="{*[1]/@id}"><xsl:value-of select="$symbol"/></m:mo>
         <xsl:apply-templates select="."/>
        </m:mrow>
       </m:mtd>
@@ -1763,9 +1769,7 @@ which generates the toplevel element (see for instance xlink) -->
 <xsl:template match = "m:set">
  <xsl:choose>
   <xsl:when test="count(child::*) = 0">
-   <m:mi> 
-    <m:mchar name="emptyset"/>
-   </m:mi>
+   <m:mi>&#x02205;</m:mi>
   </xsl:when>
   <xsl:otherwise>
    <xsl:variable name="charlength">
@@ -1945,6 +1949,3 @@ which generates the toplevel element (see for instance xlink) -->
 </xsl:template>
 
 </xsl:stylesheet> 
-
-
-
diff --git a/helm/style/params.xsl b/helm/style/params.xsl
index 8db72e23e..6e7f98545 100644
--- a/helm/style/params.xsl
+++ b/helm/style/params.xsl
@@ -309,7 +309,7 @@
      <xsl:when test="($target = 1) and ($noparams != 0)">
       <m:apply>
       <m:csymbol>app</m:csymbol>
-<!-- Mancava modalita': sono qall'interno di un termine -->
+<!-- Mancava modalita': sono all'interno di un termine -->
       <xsl:apply-templates select="." mode="pure"/>
       <xsl:call-template name="printparam"><xsl:with-param name="noleft" select="$noparams"/></xsl:call-template>
       </m:apply>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 6ed01233d..b35968891 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -575,9 +575,3 @@
 
 
 </xsl:stylesheet>
-
-
-
-
-
-
diff --git a/helm/style/reals.xsl b/helm/style/reals.xsl
index c7a6b8e02..09fd63ac2 100644
--- a/helm/style/reals.xsl
+++ b/helm/style/reals.xsl
@@ -317,5 +317,3 @@
 </xsl:template>
 
 </xsl:stylesheet>
-
-
diff --git a/helm/style/ricerca.xsl b/helm/style/ricerca.xsl
index 24f5e1746..9831718df 100644
--- a/helm/style/ricerca.xsl
+++ b/helm/style/ricerca.xsl
@@ -100,16 +100,3 @@
 </xsl:template>
 
 </xsl:stylesheet>
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/helm/style/roottheory.xsl b/helm/style/roottheory.xsl
index 38ce32460..023190b0d 100644
--- a/helm/style/roottheory.xsl
+++ b/helm/style/roottheory.xsl
@@ -42,8 +42,3 @@
 <xsl:include href="theory_content.xsl"/>
 
 </xsl:stylesheet>
-
-
-
-
-