</xsl:choose>
</xsl:for-each>
</xsl:when>
- <!-- proof -->
+ <!-- proof and side_proof -->
<xsl:when test="$name='proof' or $name='side_proof'">
<xsl:apply-templates mode="inline" select="*[position()=2]"/>
<FONT color="red"> proves </FONT>
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
+ <xsl:if test="*[4]">
+ <FONT color="red"> which is equivalent to </FONT>
+ <xsl:apply-templates mode="inline" select="*[position()=4]"/>
+ </xsl:if>
</xsl:when>
+ <!-- letin1 -->
<xsl:when test="$name='letin1'">
<xsl:text>letin1 (inline error)</xsl:text>
</xsl:when>
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:apply-templates>
</xsl:when>
- </xsl:choose>
- <xsl:choose>
<xsl:when test="name(.)='Def'">
<xsl:choose>
<xsl:when test="@name">
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:apply-templates>
</xsl:when>
+ <xsl:otherwise>
+ <xsl:text> _ :? _ </xsl:text>
+ </xsl:otherwise>
</xsl:choose>
- <xsl:otherwise>
- <xsl:text> _ :? _ </xsl:text>
- </xsl:otherwise>
</xsl:for-each>
|- <xsl:value-of select="./@no"/> :
<xsl:apply-templates select="./Goal/*[1]">