equal
deleted
inserted
replaced
12 time_use_thy "NatSum"; (*Summing integers, squares, cubes, etc.*) |
12 time_use_thy "NatSum"; (*Summing integers, squares, cubes, etc.*) |
13 time_use_thy "Ramsey"; (*Simple form of Ramsey's theorem*) |
13 time_use_thy "Ramsey"; (*Simple form of Ramsey's theorem*) |
14 time_use_thy "Limit"; (*Inverse limit construction of domains*) |
14 time_use_thy "Limit"; (*Inverse limit construction of domains*) |
15 time_use_thy "BinEx"; (*Binary integer arithmetic*) |
15 time_use_thy "BinEx"; (*Binary integer arithmetic*) |
16 |
16 |
17 (** Datatypes **) |
|
18 time_use_thy "Ntree"; (*variable-branching trees; function demo*) |
|
19 time_use_thy "Brouwer"; (*Infinite-branching trees*) |
|
20 |
|
21 (** CoDatatypes **) |
17 (** CoDatatypes **) |
22 time_use_thy "LList"; |
18 time_use_thy "LList"; |
23 time_use_thy "CoUnit"; |
19 time_use_thy "CoUnit"; |