diff -r f1c80ed70f48 -r 86b04d47b853 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Thu Mar 09 17:27:54 2000 +0100
+++ b/src/HOL/Induct/Mutil.thy	Thu Mar 09 18:27:18 2000 +0100
@@ -10,23 +10,23 @@
 
 Mutil = Main +
 
+consts     tiling :: "'a set set => 'a set set"
+inductive "tiling A"
+  intrs
+    empty  "{} : tiling A"
+    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
+
 consts    domino :: "(nat*nat)set set"
 inductive domino
   intrs
     horiz  "{(i, j), (i, Suc j)} : domino"
     vertl  "{(i, j), (Suc i, j)} : domino"
 
-consts     tiling :: "'a set set => 'a set set"
-inductive "tiling A"
-  intrs
-    empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
-
 constdefs
   below   :: "nat => nat set"
    "below n    == {i. i<n}"
   
-  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
-   "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
+  colored  :: "[nat, (nat*nat)set] => (nat*nat)set"
+   "colored b A == A Int {(i,j). (i+j) mod 2 = b}"
 
 end