src/HOL/Library/Parity.thy

 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 :: "'a::even_odd => bool" where
   "odd x == \<not> even x"
 
 
 subsection {* Even and odd are mutually exclusive *}