src/HOL/Inductive.thy
changeset 32683 7c1fe854ca6a
parent 32587 caa5ada96a00
child 32701 5059a733a4b8
     1.1 --- a/src/HOL/Inductive.thy	Fri Sep 18 14:09:38 2009 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Sat Sep 19 07:38:03 2009 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4        and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
     1.5    shows "P(a)"
     1.6    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
     1.7 -    (auto simp: inf_set_eq intro: indhyp)
     1.8 +    (auto simp: intro: indhyp)
     1.9  
    1.10  lemma lfp_ordinal_induct:
    1.11    fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
    1.12 @@ -184,7 +184,7 @@
    1.13  
    1.14  text{*strong version, thanks to Coen and Frost*}
    1.15  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
    1.16 -by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq])
    1.17 +by (blast intro: weak_coinduct [OF _ coinduct_lemma])
    1.18  
    1.19  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
    1.20    apply (rule order_trans)