changeset 30042 | 31039ee583fa |
parent 29667 | 53103fc8ffa3 |
child 30082 | 43c5b7bfc791 |
--- a/src/HOL/RealDef.thy Sat Feb 21 09:58:45 2009 +0100 +++ b/src/HOL/RealDef.thy Sat Feb 21 20:52:30 2009 +0100 @@ -655,7 +655,7 @@ real(n div d) = real n / real d" apply (frule real_of_int_div_aux [of d n]) apply simp - apply (simp add: zdvd_iff_zmod_eq_0) + apply (simp add: dvd_eq_mod_eq_0) done lemma real_of_int_div2: