src/HOL/Lambda/ListBeta.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10653 55f33da63366
     1.1 --- a/src/HOL/Lambda/ListBeta.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Lambda/ListBeta.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4    apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
     1.5    done
     1.6  
     1.7 -lemma apps_preserves_betas [rulified, simp]:
     1.8 +lemma apps_preserves_betas [rule_format, simp]:
     1.9      "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
    1.10    apply (induct_tac rs rule: rev_induct)
    1.11     apply simp