
diff -r 41aa67a045f7 -r 325300576da7 src/HOL/Induct/Mutil.thy
--- a/src/HOL/Induct/Mutil.thy	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/Induct/Mutil.thy	Wed Nov 18 15:10:46 1998 +0100
@@ -23,7 +23,7 @@
 inductive "tiling A"
   intrs
     empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
+    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
 
 defs
   below_def  "below n    == {i. i<n}"




