1.1 --- a/src/HOL/IntDiv.thy	Wed Jan 28 06:03:46 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Jan 28 16:57:12 2009 +0100
     1.3 @@ -845,12 +845,13 @@
     1.4  
     1.5  lemma zmult2_lemma_aux1: "[| (0::int) < c;  b < r;  r \<le> 0 |] ==> b*c < b*(q mod c) + r"
     1.6  apply (subgoal_tac "b * (c - q mod c) < r * 1")
     1.7 -apply (simp add: right_diff_distrib)
     1.8 + apply (simp add: algebra_simps)
     1.9  apply (rule order_le_less_trans)
    1.10 -apply (erule_tac [2] mult_strict_right_mono)
    1.11 -apply (rule mult_left_mono_neg)
    1.12 -apply (auto simp add: compare_rls add_commute [of 1]
    1.13 -                      add1_zle_eq pos_mod_bound)
    1.14 + apply (erule_tac [2] mult_strict_right_mono)
    1.15 + apply (rule mult_left_mono_neg)
    1.16 +  using add1_zle_eq[of "q mod c"]apply(simp add: algebra_simps pos_mod_bound)
    1.17 + apply (simp)
    1.18 +apply (simp)
    1.19  done
    1.20  
    1.21  lemma zmult2_lemma_aux2:
    1.22 @@ -868,12 +869,13 @@
    1.23  
    1.24  lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
    1.25  apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
    1.26 -apply (simp add: right_diff_distrib)
    1.27 + apply (simp add: right_diff_distrib)
    1.28  apply (rule order_less_le_trans)
    1.29 -apply (erule mult_strict_right_mono)
    1.30 -apply (rule_tac [2] mult_left_mono)
    1.31 -apply (auto simp add: compare_rls add_commute [of 1]
    1.32 -                      add1_zle_eq pos_mod_bound)
    1.33 + apply (erule mult_strict_right_mono)
    1.34 + apply (rule_tac [2] mult_left_mono)
    1.35 +  apply simp
    1.36 + using add1_zle_eq[of "q mod c"] apply (simp add: algebra_simps pos_mod_bound)
    1.37 +apply simp
    1.38  done
    1.39  
    1.40  lemma zmult2_lemma: "[| divmod_rel a b (q, r);  b \<noteq> 0;  0 < c |]  
    1.41 @@ -1265,7 +1267,7 @@
    1.42  
    1.43  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
    1.44    using zmod_zdiv_equality[where a="m" and b="n"]
    1.45 -  by (simp add: ring_simps)
    1.46 +  by (simp add: algebra_simps)
    1.47  
    1.48  lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
    1.49  apply (subgoal_tac "m mod n = 0")