
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 \<Longrightarrow> n * (m div n) = m"
 apply (subgoal_tac "m mod n = 0")




