First partial syncronization between the HTML and the MathML presentation:

[helm.git] / helm / style / content_to_html.xsl

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 85498997fd6bd1bcb0b4b56595d7083feb9a2f4a..6e89d8cd9aca806496587743ff5eda61e868042f 100644 (file)
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -1128,54 +1128,6 @@
         </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
-      <!-- nat_ind -->
-      <xsl:when test="$name='nat_ind_complete'">
-       <FONT color="red">By induction on&#x00a0;</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&#x00a0;</xsl:text>
-       <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 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>)&#x00a0;</xsl:text>
-       <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>
-       <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]">
@@ -1313,7 +1265,7 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       *
+       Left:&#x00a0;
        <xsl:apply-templates select="*[4]">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:apply-templates>
@@ -1321,7 +1273,7 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       *
+       Right:&#x00a0;
        <xsl:apply-templates select="*[5]">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:apply-templates>