# HG changeset patch
# User haftmann
# Date 1204894385 -3600
# Node ID 0490a5dddd27fefd4d814b9d8a44364541cf455d
# Parent  96b804999ca7ecbeb659a880ffe9aa35f1417f4f
tuned

diff -r 96b804999ca7 -r 0490a5dddd27 src/HOL/Library/Parity.thy
--- 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)"