diff -r 75df69217b57 -r c02d48a47ed1 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Mon Sep 11 20:44:53 2000 +0200
+++ b/src/HOL/Induct/Mutil.thy	Tue Sep 12 10:27:16 2000 +0200
@@ -14,7 +14,7 @@
 inductive "tiling A"
   intrs
     empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
+    Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
 
 consts    domino :: "(nat*nat)set set"
 inductive domino
@@ -23,7 +23,7 @@
     vertl  "{(i, j), (Suc i, j)} : domino"
 
 constdefs
-  colored  :: "nat => (nat*nat)set"
-   "colored b == {(i,j). (i+j) mod #2 = b}"
+  coloured  :: "nat => (nat*nat)set"
+   "coloured b == {(i,j). (i+j) mod #2 = b}"
 
 end