1.1 --- a/src/HOL/Induct/Mutil.thy	Thu Mar 09 17:27:54 2000 +0100
     1.2 +++ b/src/HOL/Induct/Mutil.thy	Thu Mar 09 18:27:18 2000 +0100
     1.3 @@ -10,23 +10,23 @@
     1.4  
     1.5  Mutil = Main +
     1.6  
     1.7 +consts     tiling :: "'a set set => 'a set set"
     1.8 +inductive "tiling A"
     1.9 +  intrs
    1.10 +    empty  "{} : tiling A"
    1.11 +    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
    1.12 +
    1.13  consts    domino :: "(nat*nat)set set"
    1.14  inductive domino
    1.15    intrs
    1.16      horiz  "{(i, j), (i, Suc j)} : domino"
    1.17      vertl  "{(i, j), (Suc i, j)} : domino"
    1.18  
    1.19 -consts     tiling :: "'a set set => 'a set set"
    1.20 -inductive "tiling A"
    1.21 -  intrs
    1.22 -    empty  "{} : tiling A"
    1.23 -    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
    1.24 -
    1.25  constdefs
    1.26    below   :: "nat => nat set"
    1.27     "below n    == {i. i<n}"
    1.28    
    1.29 -  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
    1.30 -   "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
    1.31 +  colored  :: "[nat, (nat*nat)set] => (nat*nat)set"
    1.32 +   "colored b A == A Int {(i,j). (i+j) mod 2 = b}"
    1.33  
    1.34  end