# HG changeset patch
# User huffman
# Date 1332872363 -7200
# Node ID 099397de21e3044f4beb13fec0a18e624cc8c925
# Parent  108bf76ca00c658ebe7759db5d07ce605e687739
remove more redundant lemmas

diff -r 108bf76ca00c -r 099397de21e3 NEWS
--- a/NEWS	Tue Mar 27 16:49:23 2012 +0200
+++ b/NEWS	Tue Mar 27 20:19:23 2012 +0200
@@ -156,6 +156,8 @@
   zdvd_mult_div_cancel ~> dvd_mult_div_cancel
   zmod_zmult1_eq ~> mod_mult_right_eq
   zpower_zmod ~> power_mod
+  zdvd_zmod ~> dvd_mod
+  zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd
   mod_mult_distrib ~> mult_mod_left
   mod_mult_distrib2 ~> mult_mod_right
 
diff -r 108bf76ca00c -r 099397de21e3 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Mar 27 16:49:23 2012 +0200
+++ b/src/HOL/Divides.thy	Tue Mar 27 20:19:23 2012 +0200
@@ -2132,12 +2132,6 @@
   dvd_eq_mod_eq_0 [of "neg_numeral x::int" "numeral y::int"]
   dvd_eq_mod_eq_0 [of "neg_numeral x::int" "neg_numeral y::int"] for x y
 
-lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
-  by (rule dvd_mod) (* TODO: remove *)
-
-lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
-  by (rule dvd_mod_imp_dvd) (* TODO: remove *)
-
 lemmas dvd_eq_mod_eq_0_numeral [simp] =
   dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y