X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fmmlextension.xsl;h=a22dc0dd332d56fcc2c4fcf3ee480792d3017c03;hb=4e8b137b58ec6763785b8ee490ee8cd6cb77b5bf;hp=0d23a1837ce3803999615b9cc12d8571b9af275f;hpb=f079a5948394ada2f2aba69270869058111bb3fe;p=helm.git

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index 0d23a1837..a22dc0dd3 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -420,7 +420,7 @@
        </xsl:otherwise>
        </xsl:choose> 
       </xsl:when>
-      <xsl:when test="$name='letin'">
+      <xsl:when test="$name='let_in'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
@@ -1098,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>
@@ -1223,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>