--- a/src/HOL/Integ/Parity.thy Sun Apr 09 18:51:11 2006 +0200
+++ b/src/HOL/Integ/Parity.thy Sun Apr 09 18:51:13 2006 +0200
@@ -11,22 +11,20 @@
axclass even_odd < type
-instance int :: even_odd ..
-instance nat :: even_odd ..
-
consts
even :: "'a::even_odd => bool"
-syntax
- odd :: "'a::even_odd => bool"
-
-translations
- "odd x" == "~even x"
+instance int :: even_odd ..
+instance nat :: even_odd ..
defs (overloaded)
even_def: "even (x::int) == x mod 2 = 0"
even_nat_def: "even (x::nat) == even (int x)"
+abbreviation
+ odd :: "'a::even_odd => bool"
+ "odd x == \<not> even x"
+
subsection {* Even and odd are mutually exclusive *}