src/HOL/Induct/Mutil.thy
 changeset 8399 86b04d47b853 parent 8340 c169cd21fe42 child 8589 a24f7e5ee7ef
```     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
```