X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=9113ba51c2a1643c2a0b3aee6e53a82d32c921ab;hb=71cc512008eddc1c64b0388b7def903d1994eaa2;hp=e130b4fb6aff8fceeaf5436ebcf3cb8410a61066;hpb=8e1a7e55cbc7750446f0a7ab3d071190594243fb;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index e130b4fb6..9113ba51c 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='let_in'">
+       <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>
@@ -1038,6 +1098,49 @@
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <xsl:when test="$name='ex_ind'">
+        <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:choose>
+             <xsl:when test="name(*[2])='m:apply'">
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:when>
+             <xsl:otherwise>
+              <m:mtext>Consider </m:mtext>
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:otherwise>
+            </xsl:choose>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mtext>Let</m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates select="*[3]"/>
+           <m:mtext>:</m:mtext>
+           <xsl:apply-templates select="*[4]"/>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <m:mtext>such that</m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <m:mtext>(</m:mtext>
+            <xsl:apply-templates select="*[5]"/>
+           <m:mtext>)</m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates select="*[6]"/>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:apply-templates select="*[7]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+        </m:mtable>
+      </xsl:when>
       <xsl:otherwise>
        <m:ci>ERROR</m:ci>
       </xsl:otherwise>
@@ -1069,7 +1172,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 +1190,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 +1212,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 +1227,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"/>
@@ -1163,9 +1266,7 @@
      <m:mtr>
       <m:mtd>
        <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-       <m:mo helm:xref="m:in/@helm:xref"> 
-        =
-       </m:mo>
+       <m:mo helm:xref="{m:in/@helm:xref}">=</m:mo>
        <xsl:apply-templates select="."/>
       </m:mtd>
      </m:mtr>
@@ -1429,7 +1530,7 @@
      <xsl:otherwise>
       <xsl:value-of select="number($siblength)"/>
      </xsl:otherwise>
-     </xsl:choose>>
+     </xsl:choose>
     </xsl:when>
     <xsl:otherwise>
      <xsl:value-of select="number($childlength)"/>
@@ -1441,3 +1542,4 @@
 
 </xsl:stylesheet> 
 
+