| changeset 22091 | d13ad9a479f9 |
| parent 22026 | cc60e54aa7cb |
| child 22744 | 5cbe966d67a2 |
--- a/src/HOL/Integ/IntDiv.thy Fri Jan 19 13:16:37 2007 +0100 +++ b/src/HOL/Integ/IntDiv.thy Fri Jan 19 15:13:47 2007 +0100 @@ -1243,7 +1243,7 @@ apply (simp add: mult_ac) done -lemma zdvd1_eq: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" +lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)" proof assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1) hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)