src/HOL/IMP/HoareT.thy

--- a/src/HOL/IMP/HoareT.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/HoareT.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -70,7 +70,7 @@
 apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps)
 apply clarsimp
 apply arith
-apply fastsimp
+apply fastforce
 apply(rule Semi)
 prefer 2
 apply(rule Assign)
@@ -95,7 +95,7 @@
   qed
 next
   case If thus ?case by auto blast
-qed fastsimp+
+qed fastforce+
 
 
 text{*