From: Irene Schena <irene.schena@unibo.it>
Date: Wed, 17 Jan 2001 11:33:35 +0000 (+0000)
Subject: Modified Files:
X-Git-Tag: no-uwobo~33
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f079a5948394ada2f2aba69270869058111bb3fe;p=helm.git

Modified Files:
1) annotatedcont.xsl, objcontent.xsl, proofs.xsl, rootcontent.xsl: added LETIN
2) content.xsl, mmlextension.xsl: added LETIN and body to Variable,
changed color into mathcolor
3) content_to_html.xsl, html_init.xsl, html_reals.xsl, html_set.xsl:
changed color into mathcolor
4) reals.xsl: power instead of root
---

diff --git a/helm/style/annotatedcont.xsl b/helm/style/annotatedcont.xsl
index 168dbd479..7d5a6d5b3 100644
--- a/helm/style/annotatedcont.xsl
+++ b/helm/style/annotatedcont.xsl
@@ -35,7 +35,7 @@
 
 <xsl:import href="objcontent.xsl"/>
 
-<xsl:key name="id" use="@id" match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
+<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
 
 <xsl:key name="annid" use="@of" match="Annotation"/>
 
@@ -52,7 +52,7 @@
     </xsl:choose>
 </xsl:template>
 
-<xsl:template match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
+<xsl:template match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX">
     <xsl:choose>
     <xsl:when test="key('annid',@id)">
      <annotation helm:xref="{@id}">
diff --git a/helm/style/content.xsl b/helm/style/content.xsl
index afeb75493..a8d2ae856 100644
--- a/helm/style/content.xsl
+++ b/helm/style/content.xsl
@@ -79,6 +79,19 @@ Amaya o da chi di dovere in /really_very_local/helm/PARSER/example/.../]
     </m:lambda>
 </xsl:template>
 
+<xsl:template match="LETIN" mode="pure">
+    <m:apply helm:xref="{@id}">
+     <m:csymbol>letin</m:csymbol>
+     <m:bvar>
+      <m:ci>
+       <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="letintarget/@binder"/></xsl:with-param></xsl:call-template>
+      </m:ci>
+     </m:bvar>
+     <xsl:apply-templates select="*[1]" mode="noannot"/>
+     <xsl:apply-templates select="letintarget/*[1]" mode="noannot"/>
+    </m:apply>
+</xsl:template>
+
 <xsl:template match="PROD" mode="pure">
     <m:apply helm:xref="{@id}">
      <xsl:choose>
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index d3cb77408..d352da2a9 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -122,7 +122,7 @@
        <xsl:choose>
        <xsl:when test="$charlength > $framewidth">
          <!-- &#x03a0; -->
-         <FONT FACE="symbol" SIZE="+2" color="blue">&#80;</FONT>
+         <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#80;</FONT>
          <xsl:apply-templates select="m:bvar/m:ci"/>
          <xsl:text>:</xsl:text>
          <xsl:apply-templates select="m:bvar/m:type">
@@ -139,7 +139,7 @@
        </xsl:when>
        <xsl:otherwise>
         <!-- &#x03a0; -->
-        <FONT FACE="symbol" SIZE="+2" color="blue">&#80;</FONT>
+        <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#80;</FONT>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <xsl:text>:</xsl:text>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -160,7 +160,7 @@
         <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
        </xsl:call-template>
        <!-- -> -->
-       <FONT FACE="symbol" SIZE="+2" color="blue">&#174;</FONT>
+       <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#174;</FONT>
        <xsl:apply-templates select="*[position()=3]">
         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
        </xsl:apply-templates>
@@ -170,7 +170,7 @@
         <xsl:text>(</xsl:text>
         <xsl:apply-templates select="*[position()=2]"/>
         <!-- -> -->
-        <FONT FACE="symbol" SIZE="+2" color="blue">&#174;</FONT>
+        <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#174;</FONT>
         <xsl:apply-templates select="*[position()=3]"/>
         <xsl:text>)</xsl:text>
        </xsl:otherwise>
@@ -274,7 +274,7 @@
             </xsl:otherwise>
             </xsl:choose>
             <xsl:apply-templates select="."/>
-            <FONT FACE="symbol" SIZE="+2" color="green">&#222;</FONT>
+            <FONT FACE="symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
             <xsl:apply-templates select="following-sibling::*[position()= 1]">
              <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
             </xsl:apply-templates>
@@ -294,7 +294,7 @@
          </xsl:when> 
          </xsl:choose>
          <xsl:apply-templates select="."/>
-         <FONT FACE="symbol" SIZE="+2" color="green">&#222;</FONT>
+         <FONT FACE="symbol" SIZE="+2" mathcolor="green">&#222;</FONT>
          <xsl:apply-templates select="following-sibling::*[position()= 1]">
           <xsl:with-param name="current_indent" select="$current_indent + 2 + string-length()"/>
          </xsl:apply-templates>
@@ -427,7 +427,7 @@
      <xsl:choose>
      <xsl:when test="$charlength > $framewidth">
        <!-- &#x03bb; -->
-       <FONT FACE="symbol" SIZE="+2" color="red">&#108;</FONT>
+       <FONT FACE="symbol" SIZE="+2" mathcolor="red">&#108;</FONT>
        <xsl:apply-templates select="m:bvar/m:ci"/>
        <xsl:text>:</xsl:text>
        <xsl:apply-templates select="m:bvar/m:type">
@@ -444,7 +444,7 @@
      </xsl:when>
      <xsl:otherwise>
       <!-- &#x03bb; -->
-      <FONT FACE="symbol" SIZE="+2" color="red">&#108;</FONT>
+      <FONT FACE="symbol" SIZE="+2" mathcolor="red">&#108;</FONT>
       <xsl:apply-templates select="m:bvar/m:ci"/>
       <xsl:text>:</xsl:text>
       <xsl:apply-templates select="m:bvar/m:type"/>
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index d73a48b72..0fad1aeab 100644
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -95,7 +95,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" color="blue">
+     <FONT FACE="symbol" mathcolor="blue">
       <xsl:value-of select="$symbol"/>
      </FONT>
      </a>
@@ -111,7 +111,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" color="blue">
+     <FONT FACE="symbol" mathcolor="blue">
      <xsl:value-of select="$symbol"/>
      </FONT>
      </a>
@@ -195,7 +195,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" color="blue">&#216;</FONT>
+     <FONT FACE="symbol" mathcolor="blue">&#216;</FONT>
      </a>
      <xsl:apply-templates select="*[2]"/>
  </xsl:template>
@@ -217,7 +217,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" color="blue">&#36;</FONT>
+     <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
      </a>
      <xsl:apply-templates select="m:bvar/m:ci"/>
      <xsl:text>:</xsl:text>
@@ -239,7 +239,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" color="blue">&#36;</FONT>
+     <FONT FACE="symbol" mathcolor="blue">&#36;</FONT>
      </a>
      <xsl:apply-templates select="m:bvar/m:ci"/>
      <xsl:text>:</xsl:text>
diff --git a/helm/style/html_reals.xsl b/helm/style/html_reals.xsl
index 03dd369fd..eb04dbb6f 100644
--- a/helm/style/html_reals.xsl
+++ b/helm/style/html_reals.xsl
@@ -55,7 +55,7 @@
      </a>
      <SUB>
       <xsl:apply-templates select="m:bvar/m:ci"/>
-      <FONT FACE="symbol" color="blue">&#174;</FONT>
+      <FONT FACE="symbol" mathcolor="blue">&#174;</FONT>
       <xsl:apply-templates select="m:lowlimit"/>
      </SUB>
      <BR/> 
@@ -75,7 +75,7 @@
      </a>
      <SUB>
       <xsl:apply-templates select="m:bvar/m:ci"/>
-      <FONT FACE="symbol" color="blue">&#174;</FONT>
+      <FONT FACE="symbol" mathcolor="blue">&#174;</FONT>
       <xsl:apply-templates select="m:lowlimit"/>
      </SUB>
      <xsl:apply-templates select="*[4]">
diff --git a/helm/style/html_set.xsl b/helm/style/html_set.xsl
index 5b50211df..cafdbefc4 100644
--- a/helm/style/html_set.xsl
+++ b/helm/style/html_set.xsl
@@ -59,7 +59,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#206;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#206;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -73,7 +73,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#206;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#206;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
@@ -102,7 +102,7 @@
      <xsl:call-template name="make_indent">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/> 
      </xsl:call-template>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#207;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#207;</FONT>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
      </xsl:apply-templates>
@@ -111,7 +111,7 @@
     <xsl:otherwise>
      <xsl:text>(</xsl:text>
      <xsl:apply-templates select="*[2]"/>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#207;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#207;</FONT>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
     </xsl:otherwise>
@@ -128,7 +128,7 @@
   </xsl:variable>
   <xsl:choose>
    <xsl:when test="count(child::*) = 0">
-    <FONT FACE="symbol" color="blue">&#198;</FONT>
+    <FONT FACE="symbol" mathcolor="blue">&#198;</FONT>
    </xsl:when>
    <xsl:otherwise>
     <xsl:variable name="charlength">
@@ -231,7 +231,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#199;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#199;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -245,7 +245,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#199;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#199;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
@@ -278,7 +278,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#200;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#200;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -292,7 +292,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#200;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#200;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
@@ -324,7 +324,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#205;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#205;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -338,7 +338,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#205;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#205;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
@@ -370,7 +370,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#204;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#204;</FONT>
      </a>
      <xsl:apply-templates select="*[3]">
       <xsl:with-param name="current_indent" select="$current_indent + 2"/>
@@ -384,7 +384,7 @@
      <xsl:attribute name="href">
       <xsl:value-of select="concat(string($header),string($uri))"/>
      </xsl:attribute>
-     <FONT FACE="symbol" SIZE="+2" color="blue">&#204;</FONT>
+     <FONT FACE="symbol" SIZE="+2" mathcolor="blue">&#204;</FONT>
      </a>
      <xsl:apply-templates select="*[3]"/>
      <xsl:text>)</xsl:text>
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index e130b4fb6..0d23a1837 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -319,6 +319,23 @@
         </m:mrow>
        </m:mtd>
       </m:mtr>
+      <xsl:if test="name(*[1])='body'">
+       <m:mtr>
+        <m:mtd>
+         <m:mrow>
+          <m:mtext>AS</m:mtext>
+         </m:mrow>
+        </m:mtd>
+       </m:mtr>
+       <m:mtr>
+        <m:mtd>
+         <m:mrow>
+          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
+          <xsl:apply-templates select="body/*[1]"/>
+         </m:mrow>
+        </m:mtd>
+       </m:mtr>
+      </xsl:if>
      </m:mtable>
     </m:math>
 </xsl:template>
@@ -379,7 +396,7 @@
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
-            <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
+            <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
             <xsl:apply-templates select="m:bvar"/>
           </m:mtd>
          </m:mtr>
@@ -394,7 +411,7 @@
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo color="Blue"><m:mchar name="ForAll"/></m:mo>
+        <m:mo mathcolor="Blue"><m:mchar name="ForAll"/></m:mo>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <m:mo>:</m:mo>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -403,13 +420,56 @@
        </xsl:otherwise>
        </xsl:choose> 
       </xsl:when>
+      <xsl:when test="$name='letin'">
+       <xsl:choose>
+       <xsl:when test="$charlength >= $framewidth">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+            <m:mo>LET</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="m:bvar"/>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mo>=</m:mo>
+            <xsl:apply-templates select="*[position()=3]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mo>IN</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[position()=4]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+        </m:mtable>
+       </xsl:when>
+       <xsl:otherwise>
+        <m:mo>LET</m:mo>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <xsl:apply-templates select="m:bvar/m:ci"/>
+        <m:mo>=</m:mo>
+        <xsl:apply-templates select="*[position()=3]"/>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <m:mtext>IN</m:mtext>
+        <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+        <xsl:apply-templates select="*[position()=4]"/>
+       </xsl:otherwise>
+       </xsl:choose>
+      </xsl:when> 
       <xsl:when test="$name='prod'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
-            <m:mo color="Blue">&#x03a0;</m:mo>
+            <m:mo mathcolor="Blue">&#x03a0;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
           </m:mtd>
          </m:mtr>
@@ -424,7 +484,7 @@
         </m:mtable>
        </xsl:when>
        <xsl:otherwise>
-        <m:mo color="Blue">&#x03a0;</m:mo>
+        <m:mo mathcolor="Blue">&#x03a0;</m:mo>
         <xsl:apply-templates select="m:bvar/m:ci"/>
         <m:mo>:</m:mo>
         <xsl:apply-templates select="m:bvar/m:type"/>
@@ -448,7 +508,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo color="Blue">&#x2192;</m:mo>
+            <m:mo mathmathcolor="Blue">&#x2192;</m:mo>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
@@ -465,7 +525,7 @@
        <xsl:otherwise>
         <m:mo stretchy="false">(</m:mo>
         <xsl:apply-templates select="*[position()=2]"/>
-        <m:mo color="Blue">&#x2192;</m:mo>
+        <m:mo mathcolor="Blue">&#x2192;</m:mo>
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mo stretchy="false">)</m:mo>
        </xsl:otherwise>
@@ -528,7 +588,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mo color="Maroon">:></m:mo>
+            <m:mo mathcolor="Maroon">:></m:mo>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
           </m:mtd>
@@ -545,7 +605,7 @@
        <xsl:otherwise>
         <m:mo stretchy="false">(</m:mo>
         <xsl:apply-templates select="*[position()=2]"/>
-        <m:mo color="Maroon">:></m:mo>
+        <m:mo mathcolor="Maroon">:></m:mo>
         <xsl:apply-templates select="*[position()=3]"/>
         <m:mo stretchy="false">)</m:mo>
        </xsl:otherwise>
@@ -614,7 +674,7 @@
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
             <xsl:if test="$framewidth > $charlength">
-             <m:mo color="Green">&#x21d2;</m:mo>
+             <m:mo mathcolor="Green">&#x21d2;</m:mo>
              <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
             </xsl:if>
            </m:mrow>
@@ -625,7 +685,7 @@
           <m:mtd>
            <m:mrow>
             <m:mphantom><m:mtext>|_</m:mtext></m:mphantom>  
-            <m:mo color="Green">&#x21d2;</m:mo>
+            <m:mo mathcolor="Green">&#x21d2;</m:mo>
             <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
            </m:mrow>
           </m:mtd>
@@ -655,7 +715,7 @@
          </xsl:when> 
          </xsl:choose>
          <xsl:apply-templates select="."/>
-         <m:mo color="Green">&#x21d2;</m:mo>
+         <m:mo mathcolor="Green">&#x21d2;</m:mo>
          <xsl:apply-templates select="following-sibling::*[position()= 1]"/>
         </xsl:for-each>
         <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
@@ -856,7 +916,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we proved </m:mtext>
+            <m:mtext mathcolor="Maroon">we proved </m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="*[position()=3]"/>
            </m:mrow>
@@ -1069,7 +1129,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Maroon">we get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1087,7 +1147,7 @@
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext color="Maroon">we get</m:mtext>
+            <m:mtext mathcolor="Maroon">we get</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
             <xsl:apply-templates select="."/>
            </m:mrow>
@@ -1109,7 +1169,7 @@
       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
         <m:mtr>
           <m:mtd>
-            <m:mo color="Red">&#x03bb;</m:mo>
+            <m:mo mathcolor="Red">&#x03bb;</m:mo>
             <xsl:apply-templates select="m:bvar"/>
           </m:mtd>
          </m:mtr>
@@ -1124,7 +1184,7 @@
       </m:mtable>
      </xsl:when>
      <xsl:otherwise>
-      <m:mo color="Red">&#x03bb;</m:mo>
+      <m:mo mathcolor="Red">&#x03bb;</m:mo>
       <xsl:apply-templates select="m:bvar/m:ci"/>
       <m:mo>:</m:mo>
       <xsl:apply-templates select="m:bvar/m:type"/>
@@ -1441,3 +1501,4 @@
 
 </xsl:stylesheet> 
 
+
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl
index 333a1ef9b..4ab19c854 100644
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -144,6 +144,11 @@
 
 <xsl:template match="Variable" mode="noannot"> 
     <Variable name="{@name}" helm:xref="{@id}">
+     <xsl:if test="name(*[1])='body'">
+      <body>
+       <xsl:apply-templates select="body/*"/>
+      </body>
+     </xsl:if>
      <type>
        <xsl:apply-templates select="type/*"/>
      </type>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 56ccec7fb..faf8d94ab 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -47,7 +47,7 @@
 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
 
 <!-- ALL this elements does not have inner type -->
-<xsl:template match="PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
+<xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
 <xsl:apply-templates select="." mode="pure"/>
 </xsl:template>
 
diff --git a/helm/style/reals.xsl b/helm/style/reals.xsl
index 982d4ed21..45ed5f61c 100644
--- a/helm/style/reals.xsl
+++ b/helm/style/reals.xsl
@@ -63,7 +63,7 @@
 
 
 
-<!-- Unary Operations -->
+<!-- Unary Operations and power -->
 
 <xsl:template match="APPLY[CONST[
  attribute::uri='cic:/Coq/Reals/Rdefinitions/Ropp.con' or
@@ -84,7 +84,7 @@
          <xsl:value-of select="'factorial'"/>
         </xsl:when>
         <xsl:when test="CONST/@uri='cic:/Coq/Reals/Rbase/Rsqr.con'">
-         <xsl:value-of select="'root'"/>
+         <xsl:value-of select="'power'"/>
         </xsl:when>
        </xsl:choose>
       </xsl:variable>
@@ -98,6 +98,9 @@
         </xsl:attribute>
        </xsl:element>
        <xsl:apply-templates select="*[2]" mode="noannot"/>
+       <xsl:if test="string($elem)='power'">
+        <m:cn><xsl:value-of select="*[2]/@value"/></m:cn>
+       </xsl:if>
       </m:apply>
      </xsl:when>
      <xsl:otherwise>
@@ -216,7 +219,9 @@
            </xsl:attribute>
           </m:limit>
           <m:bvar>
-           <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
+           <m:ci>
+            <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template>
+           </m:ci>
           </m:bvar>
           <m:lowlimit>
            <xsl:apply-templates select="*[5]" mode="noannot"/>
diff --git a/helm/style/rootcontent.xsl b/helm/style/rootcontent.xsl
index 7ce78dde3..c12db2732 100644
--- a/helm/style/rootcontent.xsl
+++ b/helm/style/rootcontent.xsl
@@ -41,7 +41,7 @@
 
 
 <xsl:import href="annotatedcont.xsl"/>
-<xsl:key name="id" use="@id" match="LAMBDA|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
+<xsl:key name="id" use="@id" match="LAMBDA|LETIN|PROD|CAST|REL|SORT|APPLY|VAR|META|CONST|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|Definition|Axiom|CurrentProof|InductiveDefinition|Variable"/>
 <xsl:include href="basic.xsl"/>
 <xsl:include href="set.xsl"/>
 <xsl:include href="reals.xsl"/>