| changeset 8781 | d0c2bd57a9fb |
| parent 8589 | a24f7e5ee7ef |
| child 8950 | 3e858b72fac9 |
| 8780:b0c32189b2c1 | 8781:d0c2bd57a9fb |
|---|---|
25 constdefs |
25 constdefs |
26 below :: "nat => nat set" |
26 below :: "nat => nat set" |
27 "below n == {i. i<n}" |
27 "below n == {i. i<n}" |
28 |
28 |
29 colored :: "nat => (nat*nat)set" |
29 colored :: "nat => (nat*nat)set" |
30 "colored b == {(i,j). (i+j) mod 2 = b}" |
30 "colored b == {(i,j). (i+j) mod #2 = b}" |
31 |
31 |
32 end |
32 end |