--- a/src/HOL/Library/Parity.thy Wed Mar 12 08:45:51 2008 +0100
+++ b/src/HOL/Library/Parity.thy Wed Mar 12 08:47:35 2008 +0100
@@ -16,19 +16,12 @@
odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
"odd x \<equiv> \<not> even x"
-instantiation int :: even_odd
+instantiation nat and 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)"