+<!-- SEQUENT -->
+
+<xsl:template match="Sequent">
+ <xsl:variable name="rowlines">
+ <xsl:for-each select="Decl|Def">
+ <xsl:if test="position() != last()">
+ <xsl:text>none </xsl:text>
+ </xsl:if>
+ </xsl:for-each>
+ <xsl:text>solid</xsl:text>
+ </xsl:variable>
+ <xsl:variable name="no" select="@no"/>
+ <m:math>
+ <m:mi><xsl:text>?</xsl:text><xsl:value-of select="$no"/></m:mi>
+ <m:mo>:</m:mo>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ <m:mtable align="baseline 1" equalrows="false" columnalign="left" helm:xref="{@helm:xref}" rowlines="{$rowlines}">
+ <xsl:for-each select="Decl|Def">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow helm:xref="{@helm:xref}">
+ <m:mi><xsl:value-of select="@name"/></m:mi>
+ <xsl:choose>
+ <xsl:when test="name(.) = 'Decl'">
+ <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>
+ <xsl:if test="not(Decl|Def)">
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </xsl:if>
+ <m:mtr>
+ <m:mtd>
+ <m:mrow>
+ <xsl:apply-templates select="Goal/*[1]"/>
+ </m:mrow>
+ </m:mtd>
+ </m:mtr>
+ </m:mtable>
+ </m:math>
+</xsl:template>
+