src/HOL/Lambda/InductTermi.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11639 4213422388c4
     1.1 --- a/src/HOL/Lambda/InductTermi.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Lambda/InductTermi.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  
     1.5  subsection {* Every term in IT terminates *}
     1.6  
     1.7 -lemma double_induction_lemma [rulified]:
     1.8 +lemma double_induction_lemma [rule_format]:
     1.9    "s : termi beta ==> \<forall>t. t : termi beta -->
    1.10      (\<forall>r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)"
    1.11    apply (erule acc_induct)