src/HOL/Library/Parity.thy
changeset 21404 eb85850d3eb7
parent 21263 de65ce2bfb32
child 22390 378f34b1e380
--- a/src/HOL/Library/Parity.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/Parity.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -22,7 +22,7 @@
   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"