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