1.1 --- a/src/HOL/Induct/Mutil.thy	Wed Nov 18 11:12:29 1998 +0100
     1.2 +++ b/src/HOL/Induct/Mutil.thy	Wed Nov 18 15:10:46 1998 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  inductive "tiling A"
     1.5    intrs
     1.6      empty  "{} : tiling A"
     1.7 -    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
     1.8 +    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
     1.9  
    1.10  defs
    1.11    below_def  "below n    == {i. i<n}"