equal
deleted
inserted
replaced
12 |
12 |
13 consts tiling :: "'a set set => 'a set set" |
13 consts tiling :: "'a set set => 'a set set" |
14 inductive "tiling A" |
14 inductive "tiling A" |
15 intrs |
15 intrs |
16 empty "{} : tiling A" |
16 empty "{} : tiling A" |
17 Un "[| a: A; t: tiling A; a <= -t |] ==> a Un t : tiling A" |
17 Un "[| a: A; t: tiling A; a Int t = {} |] ==> a Un t : tiling A" |
18 |
18 |
19 consts domino :: "(nat*nat)set set" |
19 consts domino :: "(nat*nat)set set" |
20 inductive domino |
20 inductive domino |
21 intrs |
21 intrs |
22 horiz "{(i, j), (i, Suc j)} : domino" |
22 horiz "{(i, j), (i, Suc j)} : domino" |
23 vertl "{(i, j), (Suc i, j)} : domino" |
23 vertl "{(i, j), (Suc i, j)} : domino" |
24 |
24 |
25 constdefs |
25 constdefs |
26 colored :: "nat => (nat*nat)set" |
26 coloured :: "nat => (nat*nat)set" |
27 "colored b == {(i,j). (i+j) mod #2 = b}" |
27 "coloured b == {(i,j). (i+j) mod #2 = b}" |
28 |
28 |
29 end |
29 end |