<xsl:template match="LAMBDA" mode="noannot">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
- <xsl:when test="//InnerTypes and @sort='Prop' and name(../..) != 'LAMBDA'">
+ <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and name(../..) != 'LAMBDA'">
<m:apply helm:xref="{@id}">
<m:csymbol>proof</m:csymbol>
<xsl:apply-templates mode="proof_transform" select="."/>
- <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
+ <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
</m:apply>
</xsl:when>
<xsl:otherwise>
<xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
- <xsl:when test="//InnerTypes and @sort='Prop'">
+ <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
<m:apply helm:xref="{@id}">
<m:csymbol>proof</m:csymbol>
<xsl:apply-templates mode="proof_transform" select="."/>
- <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
+ <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
</m:apply>
</xsl:when>
<xsl:otherwise>
<m:apply helm:xref="{@id}">
<m:csymbol>or_ind</m:csymbol>
<xsl:apply-templates mode="noannot" select="*[7]"/>
- <xsl:apply-templates mode="pure" select="//InnerTypes/TYPE[@of=$id]/*"/>
+ <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
<xsl:apply-templates mode="pure" select="*[5]"/>
<xsl:apply-templates mode="pure" select="*[6]"/>
</m:apply>
<xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
<!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
<xsl:choose>
- <xsl:when test="//InnerTypes and ($no_subproofs = 1)">
+ <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
<m:apply helm:xref="{@id}">
<m:csymbol>letin1</m:csymbol>
<xsl:apply-templates mode="noannot" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
</m:apply>
</m:apply>
</xsl:when>
- <xsl:when test="//InnerTypes and ($no_subproofs > 1)">
+ <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
<m:apply helm:xref="{@id}">
<m:csymbol>letin</m:csymbol>
<!-- first process all subproofs (let-in) -->
<xsl:template match="*" mode="previous">
<xsl:choose>
- <xsl:when test="//InnerTypes and(@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX'))">
+ <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:variable name="id" select="@id"/>
<xsl:choose>
<!-- <xsl:when test="key('typeid',@id)"> -->
- <!-- <xsl:when test="//InnerTypes/TYPE[@of=$id]"> -->
- <xsl:when test="//InnerTypes and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')">
+ <!-- <xsl:when test="$InnerTypes/InnerTypes/TYPE[@of=$id]"> -->
+ <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>
<xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$n)"/></xsl:with-param></xsl:call-template>
</m:ci>