--- a/src/HOL/Decision_Procs/MIR.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Mon Sep 12 07:55:43 2011 +0200
@@ -2733,7 +2733,7 @@
prefer 2
apply(drule minusinfinity)
apply assumption+
-apply(fastsimp)
+apply(fastforce)
apply clarsimp
apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
apply(frule_tac x = x and z=z in decr_lemma)
@@ -2741,7 +2741,7 @@
prefer 2
apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
prefer 2 apply arith
- apply fastsimp
+ apply fastforce
apply(drule (1) periodic_finite_ex)
apply blast
apply(blast dest:decr_mult_lemma)