src/HOL/IMP/Hoare_Examples.thy
changeset 44890 22f665a2e91c
parent 44177 b4b5cbca2519
child 45015 fdac1e9880eb
--- a/src/HOL/IMP/Hoare_Examples.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -59,8 +59,8 @@
 prefer 2
 apply(rule Assign)
 apply(rule Assign')
-apply(fastsimp simp: atLeastAtMostPlus1_int_conv algebra_simps)
-apply(fastsimp)
+apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps)
+apply(fastforce)
 apply(rule Semi)
 prefer 2
 apply(rule Assign)