<xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:apply-templates>
<xsl:text>> </xsl:text>
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/> </xsl:call-template>
<xsl:text>CASE </xsl:text>
<xsl:apply-templates select="*[position()=3]">
<xsl:with-param name="current_indent" select="$current_indent + 8"/>
<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
<br/>
<xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent + 2"/>
+ <xsl:with-param name="current_indent" select="$current_indent + 2"/>
</xsl:call-template>
<xsl:choose>
<xsl:when test="position() = 1">
</xsl:choose>
<xsl:apply-templates select="."/>
<FONT FACE="Symbol" SIZE="+0" mathcolor="green">Þ</FONT>
- <xsl:apply-templates select="following-sibling::*[position()= 1]">
- <xsl:with-param name="current_indent" select="$current_indent + 4 + string-length()"/>
- </xsl:apply-templates>
+ <xsl:variable name="body_size">
+ <xsl:apply-templates
+ select="following-sibling::*[1]/*[1]" mode="charcount"/>
+ </xsl:variable>
+ <xsl:choose>
+ <xsl:when test="$body_size > $framewidth">
+ <br/>
+ <xsl:call-template name="make_indent">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 8"/>
+ </xsl:call-template>
+ <xsl:apply-templates
+ select="following-sibling::*[position()= 1]">
+ <xsl:with-param name="current_indent"
+ select="$current_indent + 8"/>
+ </xsl:apply-templates>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates select="following-sibling::*[position()= 1]"
+ mode="inline" />
+ </xsl:otherwise>
+ </xsl:choose>
</xsl:for-each>
</xsl:when>
<xsl:otherwise>
<m:apply helm:xref="{@id}">
<m:csymbol>proof</m:csymbol>
<xsl:apply-templates mode="proof_transform" select="."/>
- <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
<xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
</m:apply>
</xsl:when>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
+ <xsl:when test="name()='LAMBDA'">
+ <xsl:choose>
+ <xsl:when test="(name(target/*[1])='APPLY' and
+ name(target/*[1]/*[1])='CONST' and
+ (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
+ target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
+ target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
+ and count(target/*[1]/*) = 8
+ and name(target/*[1]/*[8])='REL'
+ and target/@binder = target/*[1]/*[8]/@binder )">
+ <m:apply>
+ <m:csymbol>rw_step</m:csymbol>
+ <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
+ <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
+ <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
+ <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
+ </xsl:when>
<xsl:otherwise>
<xsl:apply-templates select="." mode="pure"/>
</xsl:otherwise>
</m:apply>
</xsl:when>
<xsl:otherwise>
- <xsl:apply-templates mode="pure" select="."/>
+ <xsl:choose>
+ <xsl:when test="@sort='Prop'">
+ <m:apply>
+ <m:csymbol>app</m:csymbol>
+ <xsl:apply-templates mode="erase" select="*[1]"/>
+ </m:apply>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:otherwise>
+ </xsl:choose>
</xsl:otherwise>
</xsl:choose>
</xsl:template>
</xsl:for-each>
</xsl:template>
+<xsl:template match="*" mode="erase">
+ <xsl:choose>
+ <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:ci>.</m:ci>
+ </xsl:otherwise>
+ </xsl:choose>
+ <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
+</xsl:template>
+
<xsl:template match="*" mode="previous">
<xsl:choose>
<xsl:when test="$naturalLanguage='yes' and(@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX'))">
<m:ci>previous</m:ci>
</xsl:when>
<xsl:otherwise>
- <xsl:apply-templates select="." mode="pure"/>
+ <xsl:choose>
+ <xsl:when test="@sort='Prop' or $naturalLanguage='no' ">
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:ci>.</m:ci>
+ </xsl:otherwise>
+ </xsl:choose>
+ <!-- <xsl:apply-templates select="." mode="pure"/> -->
</xsl:otherwise>
</xsl:choose>
<xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
</xsl:apply-templates>
</xsl:when>
<xsl:otherwise>
- <xsl:apply-templates mode="pure" select="."/>
+ <xsl:choose>
+ <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
+ <xsl:apply-templates mode="pure" select="."/>
+ </xsl:when>
+ <xsl:otherwise>
+ <m:ci>.</m:ci>
+ </xsl:otherwise>
+ </xsl:choose>
+ <!-- <xsl:apply-templates mode="pure" select="."/> -->
<xsl:apply-templates mode="flat" select="following-sibling::*[1]">
<xsl:with-param name="n" select="$n"/>
</xsl:apply-templates>