--- a/src/HOL/Library/Parity.thy Fri Mar 07 13:53:04 2008 +0100
+++ b/src/HOL/Library/Parity.thy Fri Mar 07 13:53:05 2008 +0100
@@ -16,12 +16,19 @@
odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
"odd x \<equiv> \<not> even x"
-instantiation int and nat :: even_odd
+instantiation int :: even_odd
begin
definition
even_def [presburger]: "even x \<longleftrightarrow> (x\<Colon>int) mod 2 = 0"
+instance ..
+
+end
+
+instantiation nat :: even_odd
+begin
+
definition
even_nat_def [presburger]: "even x \<longleftrightarrow> even (int x)"