redundant: dropped
authorhaftmann
Thu Oct 02 11:33:05 2014 +0200 (2014-10-02)
changeset 5851197aec08d6f28
parent 58510 c6427c9d0898
child 58512 dc4d76dfa8f0
redundant: dropped
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 02 11:33:04 2014 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu Oct 02 11:33:05 2014 +0200
     1.3 @@ -2425,16 +2425,6 @@
     1.4  
     1.5  subsubsection {* The Divides Relation *}
     1.6  
     1.7 -lemma dvd_neg_numeral_left [simp]:
     1.8 -  fixes y :: "'a::comm_ring_1"
     1.9 -  shows "(- numeral k) dvd y \<longleftrightarrow> (numeral k) dvd y"
    1.10 -  by (fact minus_dvd_iff)
    1.11 -
    1.12 -lemma dvd_neg_numeral_right [simp]:
    1.13 -  fixes x :: "'a::comm_ring_1"
    1.14 -  shows "x dvd (- numeral k) \<longleftrightarrow> x dvd (numeral k)"
    1.15 -  by (fact dvd_minus_iff)
    1.16 -
    1.17  lemmas dvd_eq_mod_eq_0_numeral [simp] =
    1.18    dvd_eq_mod_eq_0 [of "numeral x" "numeral y"] for x y
    1.19