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)