src/ZF/Induct/Mutil.thy

     empty: "0 \<in> tiling(A)"
     Un: "[| a \<in> A;  t \<in> tiling(A);  a Int t = 0 |] ==> a Un t \<in> tiling(A)"
   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}"
 
 
 subsection {* Basic properties of evnodd *}