18 time_use_thy "ex/equiv"; |
18 time_use_thy "ex/equiv"; |
19 time_use_thy "ex/integ"; |
19 time_use_thy "ex/integ"; |
20 (*Binary integer arithmetic*) |
20 (*Binary integer arithmetic*) |
21 use "ex/twos-compl.ML"; |
21 use "ex/twos-compl.ML"; |
22 time_use "ex/bin.ML"; |
22 time_use "ex/bin.ML"; |
23 time_use_thy "ex/bin-fn"; |
23 time_use_thy "ex/binfn"; |
24 |
24 |
25 (** Datatypes **) |
25 (** Datatypes **) |
26 (*binary trees*) |
26 (*binary trees*) |
27 time_use "ex/bt.ML"; |
27 time_use "ex/bt.ML"; |
28 time_use_thy "ex/bt-fn"; |
28 time_use_thy "ex/bt_fn"; |
29 (*terms: recursion over the list functor*) |
29 (*terms: recursion over the list functor*) |
30 time_use "ex/term.ML"; |
30 time_use "ex/term.ML"; |
31 time_use_thy "ex/term-fn"; |
31 time_use_thy "ex/termfn"; |
32 (*trees/forests: mutual recursion*) |
32 (*trees/forests: mutual recursion*) |
33 time_use "ex/tf.ML"; |
33 time_use "ex/tf.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*) |
39 (*mapping a relation over a list*) |
40 time_use "ex/rmap.ML"; |
40 time_use "ex/rmap.ML"; |
41 (*completeness of propositional logic*) |
41 (*completeness of propositional logic*) |
42 time_use "ex/prop.ML"; |
42 time_use "ex/prop.ML"; |
43 time_use_thy "ex/prop-log"; |
43 time_use_thy "ex/propthms"; |
44 (*two Coq examples by Ch. Paulin-Mohring*) |
44 (*two Coq examples by Ch. Paulin-Mohring*) |
45 time_use "ex/listn.ML"; |
45 time_use "ex/listn.ML"; |
46 time_use "ex/acc.ML"; |
46 time_use "ex/acc.ML"; |
47 (*Diamond property for combinatory logic*) |
47 (*Diamond property for combinatory logic*) |
48 time_use "ex/comb.ML"; |
48 time_use "ex/comb.ML"; |
50 time_use "ex/parcontract.ML"; |
50 time_use "ex/parcontract.ML"; |
51 time_use_thy "ex/primrec"; |
51 time_use_thy "ex/primrec"; |
52 |
52 |
53 (** Co-Datatypes **) |
53 (** Co-Datatypes **) |
54 time_use "ex/llist.ML"; |
54 time_use "ex/llist.ML"; |
55 time_use_thy "ex/llist-fn"; |
55 time_use "ex/llist_eq.ML"; |
|
56 time_use_thy "ex/llistfn"; |
56 |
57 |
57 |
58 |
58 maketest"END: Root file for ZF Set Theory examples"; |
59 maketest"END: Root file for ZF Set Theory examples"; |