--- a/src/HOL/IMP/AbsInt1.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy Mon Sep 12 07:55:43 2011 +0200
@@ -171,12 +171,12 @@
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
proof(induct c arbitrary: s t S)
- case SKIP thus ?case by fastsimp
+ case SKIP thus ?case by fastforce
next
case Assign thus ?case
by (auto simp: lookup_update aval'_sound)
next
- case Semi thus ?case by fastsimp
+ case Semi thus ?case by fastforce
next
case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
next