equal
deleted
inserted
replaced
13 domino :: "(nat*nat)set set" |
13 domino :: "(nat*nat)set set" |
14 tiling :: 'a set set => 'a set set |
14 tiling :: 'a set set => 'a set set |
15 below :: nat => nat set |
15 below :: nat => nat set |
16 evnodd :: "[(nat*nat)set, nat] => (nat*nat)set" |
16 evnodd :: "[(nat*nat)set, nat] => (nat*nat)set" |
17 |
17 |
18 inductive "domino" |
18 inductive domino |
19 intrs |
19 intrs |
20 horiz "{(i, j), (i, Suc j)} : domino" |
20 horiz "{(i, j), (i, Suc j)} : domino" |
21 vertl "{(i, j), (Suc i, j)} : domino" |
21 vertl "{(i, j), (Suc i, j)} : domino" |
22 |
22 |
23 inductive "tiling A" |
23 inductive "tiling A" |