changeset 44890 | 22f665a2e91c |
parent 43143 | 1aeafba76f21 |
child 52047 | 0476162187c4 |
--- a/src/HOL/HOLCF/IMP/Denotational.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/HOLCF/IMP/Denotational.thy Mon Sep 12 07:55:43 2011 +0200 @@ -48,8 +48,8 @@ lemma D_implies_eval: "!s t. D c\<cdot>(Discr s) = (Def t) --> (c,s) \<Rightarrow> t" apply (induct c) - apply fastsimp - apply fastsimp + apply fastforce + apply fastforce apply force apply (simp (no_asm)) apply force