diff -r 839db6346cc8 -r f4b83f03cac9 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Fri Jun 22 22:41:17 2007 +0200 +++ b/src/HOL/IntDiv.thy Sat Jun 23 19:33:22 2007 +0200 @@ -1210,7 +1210,7 @@ done lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)" using zmod_zdiv_equality[where a="m" and b="n"] - by (simp add: ring_eq_simps) + by (simp add: ring_simps) lemma zdvd_mult_div_cancel:"(n::int) dvd m \ n * (m div n) = m" apply (subgoal_tac "m mod n = 0")