src/ZF/Induct/Mutil.thy

--- a/src/ZF/Induct/Mutil.thy	Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/Induct/Mutil.thy	Sun Oct 07 21:19:31 2007 +0200
@@ -32,8 +32,8 @@
   type_intros empty_subsetI Union_upper Un_least PowI
   type_elims PowD [elim_format]
 
-constdefs
-  evnodd :: "[i, i] => i"
+definition
+  evnodd :: "[i, i] => i"  where
   "evnodd(A,b) == {z \<in> A. \<exists>i j. z = <i,j> \<and> (i #+ j) mod 2 = b}"