<xsl:when test="$symbol = 'arrow'">
<xsl:value-of select="'®'"/>
</xsl:when>
+ <xsl:when test="$symbol = 'RightArrow'">
+ <xsl:value-of select="'Þ'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'subst'">
+ <xsl:value-of select="'¬'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
+ <xsl:value-of select="'­'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
+ <xsl:value-of select="'®'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'beta'">
+ <xsl:value-of select="'b'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
+ <xsl:value-of select="'Þ'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'isomorphic'">
+ <xsl:value-of select="'@'"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>???</xsl:text>
+ </xsl:otherwise>
</xsl:choose>
</xsl:variable>
- <FONT FACE="symbol" SIZE="{$size}" mathcolor="{$color}">
+ <FONT FACE="symbol" SIZE="{$size}" color="{$color}">
<xsl:value-of select="$fontsymbol"/>
</FONT>
</xsl:when>
<xsl:when test="$symbol = 'arrow'">
<xsl:value-of select="'→'"/>
</xsl:when>
+ <xsl:when test="$symbol = 'RightArrow'">
+ <xsl:value-of select="'⇒'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'subst'">
+ <xsl:value-of select="'←'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'lift' or $symbol = 'lift_with_base'">
+ <xsl:value-of select="'↑'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'beta_red' or $symbol = 'beta_red1'">
+ <xsl:value-of select="'→'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'beta'">
+ <xsl:value-of select="'β'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'par_beta_red' or $symbol = 'par_beta_red1'">
+ <xsl:value-of select="'⇒'"/>
+ </xsl:when>
+ <xsl:when test="$symbol = 'isomorphic'">
+ <xsl:value-of select="'≅'"/>
+ </xsl:when>
+ <xsl:otherwise>
+ <xsl:text>???</xsl:text>
+ </xsl:otherwise>
</xsl:choose>
</xsl:variable>
<FONT color="{$color}">
<FONT color="red">CASE </FONT>
<xsl:apply-templates mode="inline" select="*[position()=3]"/>
<FONT color="red"> OF </FONT>
- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+<xsl:for-each select="piecewise/piece">
+<!--<xsl:for-each select="*[position() mod 2 = 0 and position()>3]">-->
<xsl:choose>
<xsl:when test="not(position() = 1)">
<xsl:text> | </xsl:text>
</xsl:when>
</xsl:choose>
- <xsl:apply-templates mode="inline" select="."/>
- <FONT FACE="Symbol" SIZE="+0" mathcolor="green">Þ</FONT>
+<xsl:apply-templates mode="inline" select="./*[2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'RightArrow'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<xsl:apply-templates mode="inline"
- select="following-sibling::*[position()= 1]"/>
+ select="./*[1]"/>
</xsl:for-each>
</xsl:when>
<!-- FIX -->
<xsl:text>[</xsl:text>
<xsl:apply-templates select="*[4]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>¬</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</a>
<xsl:apply-templates select="*[2]" mode="inline"/>
<xsl:text>]</xsl:text>
<xsl:apply-templates select="*[3]" mode="inline"/>
</SUB>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>­</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</a>
<SUP>
<xsl:apply-templates select="*[4]" mode="inline"/>
<xsl:when test="$name='lift'">
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>­</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</a>
<SUP>
<xsl:apply-templates select="*[2]" mode="inline"/>
<xsl:when test="$name='beta_red1'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>®</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<SUB>
- <FONT color="green" FACE="symbol">
- <xsl:text>b</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</SUB>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
<xsl:when test="$name='beta_red'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>®</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<SUB>
- <FONT color="green" FACE="symbol">
- <xsl:text>b*</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
</SUB>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
<xsl:when test="$name='par_beta_red1'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>Þ</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<SUB>
- <FONT color="green" FACE="symbol">
- <xsl:text>b</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</SUB>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
<xsl:when test="$name='par_beta_red'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>Þ</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<SUB>
- <FONT color="green" FACE="symbol">
- <xsl:text>b*</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
</SUB>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
<xsl:when test="$name='isomorphic'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>@</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
</xsl:when>
<xsl:call-template name="mksymbol-1">
<xsl:with-param name="symbol" select="$name"/>
<xsl:with-param name="color" select="'blue'"/>
- <xsl:with-param name="size" select="'+2'"/>
+ <xsl:with-param name="size" select="'+0'"/>
</xsl:call-template>
<xsl:apply-templates select="*[position()=3]">
<xsl:with-param name="current_indent" select="$current_indent + 5"/>
<xsl:with-param name="current_indent" select="$current_indent + 8"/>
</xsl:apply-templates>
<xsl:text> OF </xsl:text>
- <xsl:for-each select="*[position() mod 2 = 0 and position()>3]">
+ <xsl:for-each select="piecewise/piece">
+ <!-- <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:text>| </xsl:text>
</xsl:otherwise>
</xsl:choose>
- <xsl:apply-templates select="."/>
- <FONT FACE="Symbol" SIZE="+0" mathcolor="green">Þ</FONT>
+ <xsl:apply-templates select="./*[2]"/>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'RightArrow'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<xsl:variable name="body_size">
- <xsl:apply-templates
- select="following-sibling::*[1]/*[1]" mode="charcount"/>
+ <xsl:apply-templates
+ select="./*[1]/*[1]" mode="charcount"/>
</xsl:variable>
<xsl:choose>
<xsl:when test="$body_size > $framewidth">
<xsl:with-param name="current_indent"
select="$current_indent + 8"/>
</xsl:call-template>
- <xsl:apply-templates
- select="following-sibling::*[position()= 1]">
+<xsl:apply-templates
+ select="./*[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]"
+ <xsl:apply-templates select="./*[1]"
mode="inline" />
</xsl:otherwise>
</xsl:choose>
</xsl:otherwise>
</xsl:choose>
</xsl:when>
- <!-- nat_ind -->
- <xsl:when test="$name='nat_ind_complete'">
- <FONT color="red">By induction on </FONT>
- <xsl:apply-templates select="*[2]"/>:
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>0 </xsl:text>
- <FONT FACE="Symbol" mathcolor="green">Þ</FONT>
- <xsl:apply-templates select="*[3]">
- <xsl:with-param name="current_indent" select="$current_indent + 8"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent"/>
- </xsl:call-template>
- <xsl:text>S(</xsl:text>
- <xsl:apply-templates select="*[4]"/>
- <xsl:text>) </xsl:text>
- <FONT FACE="Symbol" mathcolor="green">Þ</FONT>
- <FONT color="red">Assume by induction</FONT>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent +10"/>
- </xsl:call-template>
- <xsl:text>(</xsl:text>
- <xsl:apply-templates select="*[5]"/>
- <xsl:text>)</xsl:text>
- <xsl:apply-templates select="*[6]">
- <xsl:with-param name="current_indent" select="$current_indent + 14"/>
- </xsl:apply-templates>
- <br/>
- <xsl:call-template name="make_indent">
- <xsl:with-param name="current_indent" select="$current_indent +10"/>
- </xsl:call-template>
- <xsl:apply-templates select="*[7]">
- <xsl:with-param name="current_indent" select="$current_indent + 10"/>
- </xsl:apply-templates>
- </xsl:when>
<!-- false_ind -->
<xsl:when test="$name='false_ind'">
<xsl:apply-templates select="*[3]">
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:call-template>
- *
+ Left: 
<xsl:apply-templates select="*[4]">
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:apply-templates>
<xsl:call-template name="make_indent">
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:call-template>
- *
+ Right: 
<xsl:apply-templates select="*[5]">
<xsl:with-param name="current_indent" select="$current_indent"/>
</xsl:apply-templates>
<xsl:text>[</xsl:text>
<xsl:apply-templates select="*[4]"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="blue" SIZE="+0" FACE="symbol">
- <xsl:text>¬</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'blue'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</a>
<xsl:apply-templates select="*[2]"/>
<xsl:text>]</xsl:text>
<xsl:apply-templates select="*[3]" mode="inline"/>
</SUB>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>­</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</a>
<SUP>
<xsl:apply-templates select="*[4]" mode="inline"/>
<xsl:when test="$name='lift'">
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>­</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</a>
<SUP>
<xsl:apply-templates select="*[2]" mode="inline"/>
<xsl:when test="$name='beta_red1'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>®</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<SUB>
- <FONT color="green" FACE="symbol">
- <xsl:text>b</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</SUB>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
<xsl:when test="$name='beta_red'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>®</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<SUB>
- <FONT color="green" FACE="symbol">
- <xsl:text>b*</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
</SUB>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
<xsl:when test="$name='par_beta_red1'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>Þ</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<SUB>
- <FONT color="green" FACE="symbol">
- <xsl:text>b</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</SUB>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
<xsl:when test="$name='par_beta_red'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>Þ</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
<SUB>
- <FONT color="green" FACE="symbol">
- <xsl:text>b*</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="'beta'"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
+ <xsl:text>*</xsl:text>
</SUB>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
<xsl:when test="$name='isomorphic'">
<xsl:apply-templates select="*[2]" mode="inline"/>
<a href="{*[1]/@definitionURL}">
- <FONT color="green" FACE="symbol">
- <xsl:text>@</xsl:text>
- </FONT>
+ <xsl:call-template name="mksymbol-1">
+ <xsl:with-param name="symbol" select="$name"/>
+ <xsl:with-param name="color" select="'green'"/>
+ <xsl:with-param name="size" select="'+0'"/>
+ </xsl:call-template>
</a>
<xsl:apply-templates select="*[3]" mode="inline"/>
</xsl:when>