src/HOL/Lambda/ListApplication.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11549 e7265e70fd7c
     1.1 --- a/src/HOL/Lambda/ListApplication.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Lambda/ListApplication.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -18,13 +18,13 @@
     1.4     apply auto
     1.5    done
     1.6  
     1.7 -lemma Var_eq_apps_conv [rulified, iff]:
     1.8 +lemma Var_eq_apps_conv [rule_format, iff]:
     1.9      "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
    1.10    apply (induct_tac ss)
    1.11     apply auto
    1.12    done
    1.13  
    1.14 -lemma Var_apps_eq_Var_apps_conv [rulified, iff]:
    1.15 +lemma Var_apps_eq_Var_apps_conv [rule_format, iff]:
    1.16      "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
    1.17    apply (induct_tac rs rule: rev_induct)
    1.18     apply simp
    1.19 @@ -69,7 +69,7 @@
    1.20     apply auto
    1.21    done
    1.22  
    1.23 -lemma Var_apps_neq_Abs_apps [rulified, iff]:
    1.24 +lemma Var_apps_neq_Abs_apps [rule_format, iff]:
    1.25      "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
    1.26    apply (induct_tac ss rule: rev_induct)
    1.27     apply simp
    1.28 @@ -103,7 +103,7 @@
    1.29  
    1.30  text {* \medskip A customized induction schema for @{text "$$"}. *}
    1.31  
    1.32 -lemma lem [rulified (no_asm)]:
    1.33 +lemma lem [rule_format (no_asm)]:
    1.34    "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
    1.35      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
    1.36    |] ==> \<forall>t. size t = n --> P t"