src/HOL/Divides.thy
changeset 47167 099397de21e3
parent 47166 108bf76ca00c
child 47217 501b9bbd0d6e
     1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 16:49:23 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 20:19:23 2012 +0200
     1.3 @@ -2132,12 +2132,6 @@
     1.4    dvd_eq_mod_eq_0 [of "neg_numeral x::int" "numeral y::int"]
     1.5    dvd_eq_mod_eq_0 [of "neg_numeral x::int" "neg_numeral y::int"] for x y
     1.6  
     1.7 -lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
     1.8 -  by (rule dvd_mod) (* TODO: remove *)
     1.9 -
    1.10 -lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
    1.11 -  by (rule dvd_mod_imp_dvd) (* TODO: remove *)
    1.12 -
    1.13  lemmas dvd_eq_mod_eq_0_numeral [simp] =
    1.14    dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
    1.15