|
1 (* Title: ZF/ex/ROOT |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Executes all examples for Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 ZF_build_completed; (*Cause examples to fail if ZF did*) |
|
10 |
|
11 writeln"Root file for ZF Set Theory examples"; |
|
12 proof_timing := true; |
|
13 |
|
14 time_use "ex/misc.ML"; |
|
15 time_use_thy "ex/ramsey"; |
|
16 |
|
17 (*Equivalence classes and integers*) |
|
18 time_use_thy "ex/equiv"; |
|
19 time_use_thy "ex/integ"; |
|
20 (*Binary integer arithmetic*) |
|
21 use "ex/twos-compl.ML"; |
|
22 time_use "ex/bin.ML"; |
|
23 time_use_thy "ex/bin-fn"; |
|
24 |
|
25 (** Datatypes **) |
|
26 (*binary trees*) |
|
27 time_use "ex/bt.ML"; |
|
28 time_use_thy "ex/bt-fn"; |
|
29 (*terms: recursion over the list functor*) |
|
30 time_use "ex/term.ML"; |
|
31 time_use_thy "ex/term-fn"; |
|
32 (*trees/forests: mutual recursion*) |
|
33 time_use "ex/tf.ML"; |
|
34 time_use_thy "ex/tf-fn"; |
|
35 (*Enormous enumeration type -- could be even bigger?*) |
|
36 time_use "ex/enum.ML"; |
|
37 |
|
38 (** Inductive definitions **) |
|
39 (*completeness of propositional logic*) |
|
40 time_use "ex/prop.ML"; |
|
41 time_use_thy "ex/prop-log"; |
|
42 (*two Coq examples by Ch. Paulin-Mohring*) |
|
43 time_use "ex/listn.ML"; |
|
44 time_use "ex/acc.ML"; |
|
45 (*Diamond property for combinatory logic*) |
|
46 time_use "ex/comb.ML"; |
|
47 time_use_thy "ex/contract"; |
|
48 time_use "ex/parcontract.ML"; |
|
49 |
|
50 (** Co-Datatypes **) |
|
51 time_use "ex/llist.ML"; |
|
52 time_use_thy "ex/llist-fn"; |
|
53 |
|
54 |
|
55 maketest"END: Root file for ZF Set Theory examples"; |