1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -2733,7 +2733,7 @@
     1.4  prefer 2
     1.5  apply(drule minusinfinity)
     1.6  apply assumption+
     1.7 -apply(fastsimp)
     1.8 +apply(fastforce)
     1.9  apply clarsimp
    1.10  apply(subgoal_tac "!!k. 0<=k \<Longrightarrow> !x. P x \<longrightarrow> P (x - k*D)")
    1.11  apply(frule_tac x = x and z=z in decr_lemma)
    1.12 @@ -2741,7 +2741,7 @@
    1.13  prefer 2
    1.14  apply(subgoal_tac "0 <= (\<bar>x - z\<bar> + 1)")
    1.15  prefer 2 apply arith
    1.16 - apply fastsimp
    1.17 + apply fastforce
    1.18  apply(drule (1)  periodic_finite_ex)
    1.19  apply blast
    1.20  apply(blast dest:decr_mult_lemma)