| changeset 1824 | 44254696843a |
| parent 1789 | aade046ec6d5 |
| child 2513 | d708d8cdc8e8 |
| 1823:e1458e1a9f80 | 1824:44254696843a |
|---|---|
24 intrs |
24 intrs |
25 empty "{} : tiling A" |
25 empty "{} : tiling A" |
26 Un "[| a: A; t: tiling A; a Int t = {} |] ==> a Un t : tiling A" |
26 Un "[| a: A; t: tiling A; a Int t = {} |] ==> a Un t : tiling A" |
27 |
27 |
28 defs |
28 defs |
29 below_def "below n == nat_rec n {} insert" |
29 below_def "below n == nat_rec {} insert n" |
30 evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}" |
30 evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}" |
31 |
31 |
32 end |
32 end |