src/HOL/Divides.thy
changeset 44890 22f665a2e91c
parent 44766 d4d33a4d7548
child 45231 d85a2fdc586c
     1.1 --- a/src/HOL/Divides.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4  apply (unfold dvd_def)
     1.5  apply auto
     1.6   apply(blast intro:mult_assoc[symmetric])
     1.7 -apply(fastsimp simp add: mult_assoc)
     1.8 +apply(fastforce simp add: mult_assoc)
     1.9  done
    1.10  
    1.11  lemma dvd_mod_imp_dvd: "[| k dvd m mod n;  k dvd n |] ==> k dvd m"
    1.12 @@ -2232,7 +2232,7 @@
    1.13  
    1.14  lemma zmod_le_nonneg_dividend: "(m::int) \<ge> 0 ==> m mod k \<le> m"
    1.15  apply (rule split_zmod[THEN iffD2])
    1.16 -apply(fastsimp dest: q_pos_lemma intro: split_mult_pos_le)
    1.17 +apply(fastforce dest: q_pos_lemma intro: split_mult_pos_le)
    1.18  done
    1.19  
    1.20