diff -r 6d29a873141f -r 05629f28f0f7 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Sun Mar 01 10:24:57 2009 +0100
+++ b/src/HOL/IntDiv.thy	Sun Mar 01 12:01:57 2009 +0100
@@ -689,9 +689,6 @@
 apply (blast intro: divmod_rel_div_mod [THEN zmult1_lemma, THEN divmod_rel_mod])
 done
 
-lemma zdiv_zmult_self1 [simp]: "b \<noteq> (0::int) ==> (a*b) div b = a"
-by (simp add: zdiv_zmult1_eq)
-
 lemma zmod_zdiv_trivial: "(a mod b) div b = (0::int)"
 apply (case_tac "b = 0", simp)
 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
@@ -717,7 +714,7 @@
   assume not0: "b \<noteq> 0"
   show "(a + c * b) div b = c + a div b"
     unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
-      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial)
+      by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
 qed auto
 
 lemma posDivAlg_div_mod: