diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/NumberTheory/EvenOdd.thy
--- a/src/HOL/NumberTheory/EvenOdd.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/NumberTheory/EvenOdd.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -8,9 +8,11 @@
 theory EvenOdd imports Int2 begin
 
 definition
-  zOdd    :: "int set"
+  zOdd    :: "int set" where
   "zOdd = {x. \<exists>k. x = 2 * k + 1}"
-  zEven   :: "int set"
+
+definition
+  zEven   :: "int set" where
   "zEven = {x. \<exists>k. x = 2 * k}"
 
 subsection {* Some useful properties about even and odd *}