]> matita.cs.unibo.it Git - helm.git/commitdiff
instantiate for inductive principles covered
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 6 Dec 2002 16:05:48 +0000 (16:05 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 6 Dec 2002 16:05:48 +0000 (16:05 +0000)
helm/style/proofs.xsl

index 65de766d1bb65d787267518f7509cd57a92fcdfc..6f49a2678db95f6c33454fb75819f42db5a4015e 100644 (file)
   <xsl:when test="name()='APPLY'">
    <xsl:variable name="id" select="@id"/>
    <xsl:choose>
-    <xsl:when test="name(*[1])='CONST'">
+    <xsl:when test="name(*[1])='CONST' or 
+      (name(*[1])='instantiate' and name(*[1]/*[1])='CONST')">
      <xsl:apply-templates mode="try_inductive" select="."/>
     </xsl:when>
     <!-- patch temporanea per la gestione di redex -->