# HG changeset patch
# User huffman
# Date 1231832190 28800
# Node ID b2cfb5d0a59e1c8874727dbfb2e2fea043b98eb8
# Parent  c0d225a7f6ff5479ebd969af546b38d39c1fd2ed
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)

diff -r c0d225a7f6ff -r b2cfb5d0a59e src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Jan 12 22:41:08 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Mon Jan 12 23:36:30 2009 -0800
@@ -295,7 +295,7 @@
 subclass ring_1 ..
 subclass comm_semiring_1_cancel ..
 
-lemma dvd_minus_iff [iff]: "x dvd - y \<longleftrightarrow> x dvd y"
+lemma dvd_minus_iff [simp]: "x dvd - y \<longleftrightarrow> x dvd y"
 proof
   assume "x dvd - y"
   then have "x dvd - 1 * - y" by (rule dvd_mult)
@@ -306,7 +306,7 @@
   then show "x dvd - y" by simp
 qed
 
-lemma minus_dvd_iff [iff]: "- x dvd y \<longleftrightarrow> x dvd y"
+lemma minus_dvd_iff [simp]: "- x dvd y \<longleftrightarrow> x dvd y"
 proof
   assume "- x dvd y"
   then obtain k where "y = - x * k" ..