4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Executes all examples for Zermelo-Fraenkel Set Theory |
6 Executes all examples for Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 ZF_build_completed; (*Cause examples to 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 "ex/misc.ML"; |
14 time_use "ex/misc.ML"; |
34 time_use_thy "ex/tf-fn"; |
34 time_use_thy "ex/tf-fn"; |
35 (*Enormous enumeration type -- could be even bigger?*) |
35 (*Enormous enumeration type -- could be even bigger?*) |
36 time_use "ex/enum.ML"; |
36 time_use "ex/enum.ML"; |
37 |
37 |
38 (** Inductive definitions **) |
38 (** Inductive definitions **) |
|
39 (*mapping a relation over a list*) |
|
40 time_use "ex/rmap.ML"; |
39 (*completeness of propositional logic*) |
41 (*completeness of propositional logic*) |
40 time_use "ex/prop.ML"; |
42 time_use "ex/prop.ML"; |
41 time_use_thy "ex/prop-log"; |
43 time_use_thy "ex/prop-log"; |
42 (*two Coq examples by Ch. Paulin-Mohring*) |
44 (*two Coq examples by Ch. Paulin-Mohring*) |
43 time_use "ex/listn.ML"; |
45 time_use "ex/listn.ML"; |
44 time_use "ex/acc.ML"; |
46 time_use "ex/acc.ML"; |
45 (*Diamond property for combinatory logic*) |
47 (*Diamond property for combinatory logic*) |
46 time_use "ex/comb.ML"; |
48 time_use "ex/comb.ML"; |
47 time_use_thy "ex/contract"; |
49 time_use_thy "ex/contract"; |
48 time_use "ex/parcontract.ML"; |
50 time_use "ex/parcontract.ML"; |
|
51 time_use_thy "ex/primrec"; |
49 |
52 |
50 (** Co-Datatypes **) |
53 (** Co-Datatypes **) |
51 time_use "ex/llist.ML"; |
54 time_use "ex/llist.ML"; |
52 time_use_thy "ex/llist-fn"; |
55 time_use_thy "ex/llist-fn"; |
53 |
56 |