First partial syncronization between the HTML and the MathML presentation:

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

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index a0302bde6a2bd04cdaa9a45d809364a245bd5662..6ed01233d8d38c283c8111af71bdf1b3dd197010 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -157,32 +157,6 @@
   <xsl:when test="name()='APPLY'">
    <xsl:variable name="id" select="@id"/>
    <xsl:choose>
-    <!-- NATIND 3 parametri -->
-    <xsl:when test="CONST[attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con']              and count(child::*) = 4">
-     <m:apply>
-      <m:csymbol>nat_ind</m:csymbol>
-      <xsl:apply-templates mode="noannot" select="*[3]"/>
-      <xsl:apply-templates mode="noannot" select="*[4]"/>
-     </m:apply>
-    </xsl:when>
-    <!-- NATIND 4 parametri (nuova versione) -->
-    <!-- 
-    <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] 
- and count(child::*) = 5
- and name(*[4])='LAMBDA' 
- and name(*[4]/target/*[1])='LAMBDA'"> 
-     <m:apply>
-      <m:csymbol>nat_ind_complete</m:csymbol>
-      <xsl:apply-templates mode="noannot" select="*[5]"/>
-      <xsl:apply-templates mode="noannot" select="*[3]"/>
-      <m:ci><xsl:value-of select="*[4]/target/@binder"/></m:ci>
-      <m:ci><xsl:value-of select="*[4]/target/*[1]/target/@binder"/></m:ci>
-      <xsl:apply-templates mode="noannot" select="*[4]/target/*[1]/source/*"/>
-      <xsl:apply-templates mode="noannot" select="*[4]/target/*[1]/target/*"/>
-     </m:apply>
-    </xsl:when> 
-    -->
     <!-- EQUALITY -->
     <xsl:when test="CONST[
  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or