Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
declare dvd_minus_iff and minus_dvd_iff [iff]
authorhuffman
Mon, 12 Jan 2009 12:10:41 -0800
changeset 29461 7c1841a7bdf4
parent 29460 ad87e5d1488b
child 29462 dc97c6188a7a
declare dvd_minus_iff and minus_dvd_iff [iff]
src/HOL/Ring_and_Field.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Ring_and_Field.thy	Mon Jan 12 12:09:54 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Mon Jan 12 12:10:41 2009 -0800
@@ -295,7 +295,7 @@
 subclass ring_1 ..
 subclass comm_semiring_1_cancel ..
 
-lemma dvd_minus_iff: "x dvd - y \<longleftrightarrow> x dvd y"
+lemma dvd_minus_iff [iff]: "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: "- x dvd y \<longleftrightarrow> x dvd y"
+lemma minus_dvd_iff [iff]: "- x dvd y \<longleftrightarrow> x dvd y"
 proof
   assume "- x dvd y"
   then obtain k where "y = - x * k" ..
isabelle