<xsl:variable name="name"><xsl:value-of select="m:csymbol"/></xsl:variable>
<xsl:variable name="charlength"><xsl:apply-templates select="m:csymbol" mode="charcount"/></xsl:variable>
<m:mrow>
- <xsl:if test="@helm:xref">
+ <xsl:if test="@id">
<xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
</xsl:if>
<xsl:choose>
<!-- subst -->
<xsl:when test="$name='subst'">
<xsl:apply-templates select="*[3]"/>
- <m:mo></m:mo>
- <m:mrow>
- <m:mo stretchy="false">[</m:mo>
- <m:mrow>
- <xsl:apply-templates select="*[4]"/>
- <m:mo mathcolor="green">
- <xsl:if test="$id != ''">
- <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
- </xsl:if>←</m:mo>
- <xsl:apply-templates select="*[2]"/>
- </m:mrow>
- <m:mo stretchy="false">]</m:mo>
- </m:mrow>
+<!-- no font for ApplyFunction: <m:mo></m:mo> -->
+ <m:mo stretchy="false">[</m:mo>
+ <xsl:apply-templates select="*[4]"/>
+ <m:mo mathcolor="green">
+ <xsl:if test="$id != ''">
+ <xsl:attribute name="m:xref"><xsl:value-of select="$id"/></xsl:attribute>
+ </xsl:if>←</m:mo>
+ <xsl:apply-templates select="*[2]"/>
+ <m:mo stretchy="false">]</m:mo>
</xsl:when>
<!-- lift -->
<xsl:when test="$name='lift'">
<xsl:choose>
<xsl:when test="$charlength >= $framewidth">
<m:mtable align="baseline 1" equalrows="false" columnalign="left">
- <xsl:if test="@helm:xref">
+ <xsl:if test="@id">
<xsl:attribute name="m:xref">
<xsl:value-of select="@id"/>
</xsl:attribute>
<m:mtd>
<m:mrow>
<m:mphantom><m:mtext>__</m:mtext></m:mphantom>
- <m:mo m:xref="{m:in/@id}">=</m:mo>
+ <m:mo>
+ <xsl:if test="m:in/@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="m:in/@id"/>
+ </xsl:attribute>
+ </xsl:if>=</m:mo>
<xsl:apply-templates select="."/>
</m:mrow>
</m:mtd>
<xsl:choose>
<xsl:when test="$charlength >= $framewidth">
<m:mtable align="baseline 1" equalrows="false" columnalign="left">
- <xsl:if test="@helm:xref">
+ <xsl:if test="@id">
<xsl:attribute name="m:xref">
<xsl:value-of select="@id"/>
</xsl:attribute>
<m:mtd>
<m:mrow>
<m:mphantom><m:mtext>__</m:mtext></m:mphantom>
- <m:mo m:xref="{*[1]/@id}"><xsl:value-of select="$symbol"/></m:mo>
+ <m:mo>
+ <xsl:if test="*[1]/@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="*[1]/@id"/>
+ </xsl:attribute>
+ </xsl:if><xsl:value-of select="$symbol"/></m:mo>
<xsl:apply-templates select="."/>
</m:mrow>
</m:mtd>
<xsl:template match = "m:set">
<xsl:choose>
<xsl:when test="count(child::*) = 0">
- <m:mi>∅</m:mi>
+ <m:mi>
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>∅</m:mi>
</xsl:when>
<xsl:otherwise>
<xsl:variable name="charlength">
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mo stretchy="false">{</m:mo>
+ <m:mo stretchy="false">
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>{</m:mo>
<xsl:apply-templates select="*[position()=1]"/>
</m:mrow>
</m:mtd>
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mo stretchy="false">}</m:mo>
+ <m:mo stretchy="false">
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>}</m:mo>
</m:mrow>
</m:mtd>
</m:mtr>
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mo stretchy="false">{</m:mo>
+ <m:mo stretchy="false">
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>{</m:mo>
<xsl:apply-templates select="*[position()=1]"/>
<xsl:if test="position() != last()">
<mo>,</mo>
<m:mtr>
<m:mtd>
<m:mrow>
- <m:mo stretchy="false">}</m:mo>
+ <m:mo stretchy="false">
+ <xsl:if test="@id">
+ <xsl:attribute name="m:xref">
+ <xsl:value-of select="@id"/>
+ </xsl:attribute>
+ </xsl:if>}</m:mo>
</m:mrow>
</m:mtd>
</m:mtr>
</m:mfenced>
</xsl:template>
-<!-- *********************************** -->
-<!-- PROOF ELEMENTS -->
-<!-- *********************************** -->
-
-
<!--**********************-->
<!-- COUNTING -->