equal
deleted
inserted
replaced
4 Copyright 2001 University of Cambridge |
4 Copyright 2001 University of Cambridge |
5 |
5 |
6 Inductive definitions. |
6 Inductive definitions. |
7 *) |
7 *) |
8 |
8 |
9 time_use_thy "Datatypes"; |
9 (** Datatypes **) |
10 time_use_thy "Binary_Trees"; |
10 time_use_thy "Datatypes"; (*sample datatypes*) |
|
11 time_use_thy "Binary_Trees"; (*binary trees*) |
11 time_use_thy "Term"; (*recursion over the list functor*) |
12 time_use_thy "Term"; (*recursion over the list functor*) |
|
13 time_use_thy "Ntree"; (*variable-branching trees; function demo*) |
12 time_use_thy "Tree_Forest"; (*mutual recursion*) |
14 time_use_thy "Tree_Forest"; (*mutual recursion*) |
|
15 time_use_thy "Brouwer"; (*Infinite-branching trees*) |
13 time_use_thy "Mutil"; (*mutilated chess board*) |
16 time_use_thy "Mutil"; (*mutilated chess board*) |
14 |
17 |
15 (*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for |
18 (*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for |
16 finite sets*) |
19 finite sets*) |
17 time_use_thy "Multiset"; |
20 time_use_thy "Multiset"; |