Theorem "(x::int) dvd 1 = ( ?x? = 1)" added to default simpset.
This solves the goals like "~ 4 dvd 1". This used to fail before.
1.1 --- a/src/HOL/Integ/IntDiv.thy Fri Jan 19 13:16:37 2007 +0100
1.2 +++ b/src/HOL/Integ/IntDiv.thy Fri Jan 19 15:13:47 2007 +0100
1.3 @@ -1243,7 +1243,7 @@
1.4 apply (simp add: mult_ac)
1.5 done
1.6
1.7 -lemma zdvd1_eq: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
1.8 +lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
1.9 proof
1.10 assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
1.11 hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)