changeset 44890 | 22f665a2e91c |
parent 44177 | b4b5cbca2519 |
child 45015 | fdac1e9880eb |
--- 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{*