1) Sequent object added.

[helm.git] / helm / style / mmlextension.xsl

diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index b9cd3165ef2bc2e4d1e98ed03d4fb4ce686950a6..f92205008f00708b89415de1a5adb9c55ed34896 100644 (file)
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -183,7 +183,8 @@ which generates the toplevel element (see for instance xlink) -->
        <m:mtd>
         <m:mrow>
          <m:mphantom><m:mtext>__</m:mtext></m:mphantom>
-         <m:mtext><xsl:value-of select="./@no"/>:</m:mtext>
+         <m:msub><m:mi>?</m:mi><m:mn><xsl:value-of select="@no"/></m:mn></m:msub>
+         <m:mtext>:</m:mtext>
          <xsl:apply-templates select="./*[1]"/>
         </m:mrow>
        </m:mtd>
@@ -192,7 +193,7 @@ which generates the toplevel element (see for instance xlink) -->
       <m:mtr>
        <m:mtd>
         <m:mrow>
-         <m:mtext>CORRESPONDING PROOF:</m:mtext>
+         <m:mtext>PROOF:</m:mtext>
         </m:mrow>
        </m:mtd>
       </m:mtr>
@@ -360,6 +361,47 @@ which generates the toplevel element (see for instance xlink) -->
     </m:math>
 </xsl:template>
 
+<!-- SEQUENT -->
+
+<xsl:template match="Sequent">
+    <m:math>
+     <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}">
+      <xsl:for-each select="Declaration|Definition">
+       <m:mtr>
+        <m:mtd>
+         <m:mrow>
+          <m:mi><xsl:value-of select="@name"/></m:mi>
+          <xsl:choose>
+           <xsl:when test="name(.) = 'Declaration'">
+            <m:mo>:</m:mo>
+           </xsl:when>
+           <xsl:otherwise>
+            <m:mo>:=</m:mo>
+           </xsl:otherwise>
+          </xsl:choose>
+          <xsl:apply-templates select="*[1]"/>
+         </m:mrow>
+        </m:mtd>
+       </m:mtr>
+      </xsl:for-each>
+      <m:mtr>
+       <m:mtd>
+        <m:mrow>
+         <m:mtext>========================================</m:mtext>
+        </m:mrow>
+       </m:mtd>
+      </m:mtr>
+      <m:mtr>
+       <m:mtd>
+        <m:mrow>
+         <xsl:apply-templates select="Goal/*[1]"/>
+        </m:mrow>
+       </m:mtd>
+      </m:mtr>
+     </m:mtable>
+    </m:math>
+</xsl:template>
+
 <!--**********************-->
 <!--        TERMS         -->
 <!--**********************-->