| changeset 23477 | f4b83f03cac9 |
| parent 23431 | 25ca91279a9b |
| child 23512 | 770e7f9f715b |
--- 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")