1.1 --- a/src/ZF/WF.thy	Sat Mar 17 12:00:11 2012 +0100
     1.2 +++ b/src/ZF/WF.thy	Sat Mar 17 12:36:11 2012 +0000
     1.3 @@ -57,7 +57,7 @@
     1.4  lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
     1.5  by (unfold wf_def wf_on_def, force)
     1.6  
     1.7 -lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)";
     1.8 +lemma wf_on_imp_wf: "[|wf[A](r); r \<subseteq> A*A|] ==> wf(r)"
     1.9  by (simp add: wf_on_def subset_Int_iff)
    1.10  
    1.11  lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
    1.12 @@ -105,7 +105,7 @@
    1.13  
    1.14  text{*Consider the least @{term z} in @{term "domain(r)"} such that
    1.15    @{term "P(z)"} does not hold...*}
    1.16 -lemma wf_induct [induct set: wf]:
    1.17 +lemma wf_induct_raw:
    1.18      "[| wf(r);
    1.19          !!x.[| \<forall>y. <y,x>: r \<longrightarrow> P(y) |] ==> P(x) |]
    1.20       ==> P(a)"
    1.21 @@ -114,7 +114,7 @@
    1.22  apply blast
    1.23  done
    1.24  
    1.25 -lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]
    1.26 +lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf]
    1.27  
    1.28  text{*The form of this rule is designed to match @{text wfI}*}
    1.29  lemma wf_induct2:
    1.30 @@ -128,7 +128,7 @@
    1.31  lemma field_Int_square: "field(r \<inter> A*A) \<subseteq> A"
    1.32  by blast
    1.33  
    1.34 -lemma wf_on_induct [consumes 2, induct set: wf_on]:
    1.35 +lemma wf_on_induct_raw [consumes 2, induct set: wf_on]:
    1.36      "[| wf[A](r);  a \<in> A;
    1.37          !!x.[| x \<in> A;  \<forall>y\<in>A. <y,x>: r \<longrightarrow> P(y) |] ==> P(x)
    1.38       |]  ==>  P(a)"
    1.39 @@ -137,8 +137,8 @@
    1.40  apply (rule field_Int_square, blast)
    1.41  done
    1.42  
    1.43 -lemmas wf_on_induct_rule =
    1.44 -  wf_on_induct [rule_format, consumes 2, induct set: wf_on]
    1.45 +lemmas wf_on_induct =
    1.46 +  wf_on_induct_raw [rule_format, consumes 2, case_names step, induct set: wf_on]
    1.47  
    1.48  
    1.49  text{*If @{term r} allows well-founded induction
    1.50 @@ -297,6 +297,7 @@
    1.51   apply (rule lam_type [THEN restrict_type2])
    1.52    apply blast
    1.53   apply (blast dest: transD)
    1.54 +apply atomize
    1.55  apply (frule spec [THEN mp], assumption)
    1.56  apply (subgoal_tac "<xa,a1> \<in> r")
    1.57   apply (drule_tac x1 = xa in spec [THEN mp], assumption)