src/HOL/Inductive.thy
changeset 41081 fb1e5377143d
parent 39776 cde508d2eac8
child 43324 2b47822868e4
     1.1 --- a/src/HOL/Inductive.thy	Wed Dec 08 14:52:23 2010 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Dec 08 14:52:23 2010 +0100
     1.3 @@ -217,7 +217,8 @@
     1.4  lemma coinduct3: 
     1.5    "[| mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"
     1.6  apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
     1.7 -apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto)
     1.8 +apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
     1.9 +apply (simp_all)
    1.10  done
    1.11  
    1.12