1 (* Title: ZF/ex/ROOT |
1 (* Title: ZF/ex/ROOT |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Executes miscellaneous examples for Zermelo-Fraenkel Set Theory |
6 Executes miscellaneous examples for Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 ZF_build_completed; (*Make examples fail if ZF did*) |
9 ZF_build_completed; (*Make examples fail if ZF did*) |
10 |
10 |
11 writeln"Root file for ZF Set Theory examples"; |
11 writeln"Root file for ZF Set Theory examples"; |
12 proof_timing := true; |
12 proof_timing := true; |
13 |
13 |
14 time_use "misc.ML"; |
14 time_use "misc.ML"; |
17 |
17 |
18 (*Integers & Binary integer arithmetic*) |
18 (*Integers & Binary integer arithmetic*) |
19 time_use_thy "Bin"; |
19 time_use_thy "Bin"; |
20 |
20 |
21 (** Datatypes **) |
21 (** Datatypes **) |
22 time_use_thy "BT"; (*binary trees*) |
22 time_use_thy "BT"; (*binary trees*) |
23 time_use_thy "Data"; (*Sample datatype*) |
23 time_use_thy "Data"; (*Sample datatype*) |
24 time_use_thy "Term"; (*terms: recursion over the list functor*) |
24 time_use_thy "Term"; (*terms: recursion over the list functor*) |
25 time_use_thy "TF"; (*trees/forests: mutual recursion*) |
25 time_use_thy "TF"; (*trees/forests: mutual recursion*) |
26 time_use_thy "Ntree"; (*variable-branching trees; function demo*) |
26 time_use_thy "Ntree"; (*variable-branching trees; function demo*) |
27 time_use_thy "Brouwer"; (*Infinite-branching trees*) |
27 time_use_thy "Brouwer"; (*Infinite-branching trees*) |
28 time_use_thy "Enum"; (*Enormous enumeration type*) |
28 time_use_thy "Enum"; (*Enormous enumeration type*) |
29 |
29 |
30 (** Inductive definitions **) |
30 (** Inductive definitions **) |
31 time_use_thy "Rmap"; (*mapping a relation over a list*) |
31 time_use_thy "Rmap"; (*mapping a relation over a list*) |
32 time_use_thy "PropLog"; (*completeness of propositional logic*) |
32 time_use_thy "PropLog"; (*completeness of propositional logic*) |
33 (*two Coq examples by Christine Paulin-Mohring*) |
33 (*two Coq examples by Christine Paulin-Mohring*) |
34 time_use_thy "ListN"; |
34 time_use_thy "ListN"; |
35 time_use_thy "Acc"; |
35 time_use_thy "Acc"; |
36 time_use_thy "Comb"; (*Combinatory Logic example*) |
36 time_use_thy "Comb"; (*Combinatory Logic example*) |
37 time_use_thy "Primrec"; (*Primitive recursive functions*) |
37 time_use_thy "Primrec"; (*Primitive recursive functions*) |
38 |
38 |
39 (** CoDatatypes **) |
39 (** CoDatatypes **) |
40 time_use_thy "LList"; |
40 time_use_thy "LList"; |
41 time_use_thy "CoUnit"; |
41 time_use_thy "CoUnit"; |
42 |
42 |