# HG changeset patch
# User haftmann
# Date 1412242385 -7200
# Node ID 97aec08d6f286b93ac99a4749d952263bd3c971a
# Parent  c6427c9d0898f7761780b43ec028fd479d9a6e88
redundant: dropped

diff -r c6427c9d0898 -r 97aec08d6f28 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Oct 02 11:33:04 2014 +0200
+++ b/src/HOL/Divides.thy	Thu Oct 02 11:33:05 2014 +0200
@@ -2425,16 +2425,6 @@
 
 subsubsection {* The Divides Relation *}
 
-lemma dvd_neg_numeral_left [simp]:
-  fixes y :: "'a::comm_ring_1"
-  shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
-  by (fact minus_dvd_iff)
-
-lemma dvd_neg_numeral_right [simp]:
-  fixes x :: "'a::comm_ring_1"
-  shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
-  by (fact dvd_minus_iff)
-
 lemmas dvd_eq_mod_eq_0_numeral [simp] =
   dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y