1.1 --- a/NEWS Tue Mar 27 16:49:23 2012 +0200
1.2 +++ b/NEWS Tue Mar 27 20:19:23 2012 +0200
1.3 @@ -156,6 +156,8 @@
1.4 zdvd_mult_div_cancel ~> dvd_mult_div_cancel
1.5 zmod_zmult1_eq ~> mod_mult_right_eq
1.6 zpower_zmod ~> power_mod
1.7 + zdvd_zmod ~> dvd_mod
1.8 + zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
1.9 mod_mult_distrib ~> mult_mod_left
1.10 mod_mult_distrib2 ~> mult_mod_right
1.11
2.1 --- a/src/HOL/Divides.thy Tue Mar 27 16:49:23 2012 +0200
2.2 +++ b/src/HOL/Divides.thy Tue Mar 27 20:19:23 2012 +0200
2.3 @@ -2132,12 +2132,6 @@
2.4 dvd_eq_mod_eq_0 [of "neg_numeral x::int" "numeral y::int"]
2.5 dvd_eq_mod_eq_0 [of "neg_numeral x::int" "neg_numeral y::int"] for x y
2.6
2.7 -lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
2.8 - by (rule dvd_mod) (* TODO: remove *)
2.9 -
2.10 -lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
2.11 - by (rule dvd_mod_imp_dvd) (* TODO: remove *)
2.12 -
2.13 lemmas dvd_eq_mod_eq_0_numeral [simp] =
2.14 dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
2.15