src/HOL/Inductive.thy
changeset 55604 42e4e8c2e8dc
parent 55575 a5e33e18fb5c
child 56146 8453d35e4684
     1.1 --- a/src/HOL/Inductive.thy	Thu Feb 20 13:53:26 2014 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Thu Feb 20 15:14:37 2014 +0100
     1.3 @@ -177,12 +177,13 @@
     1.4  
     1.5  text{*strong version, thanks to Coen and Frost*}
     1.6  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
     1.7 -  by (blast intro: weak_coinduct [OF _ coinduct_lemma])
     1.8 +  by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
     1.9  
    1.10  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
    1.11    apply (rule order_trans)
    1.12    apply (rule sup_ge1)
    1.13 -  apply (erule gfp_upperbound [OF coinduct_lemma])
    1.14 +  apply (rule gfp_upperbound)
    1.15 +  apply (erule coinduct_lemma)
    1.16    apply assumption
    1.17    done
    1.18