equal
deleted
inserted
replaced
5 |
5 |
6 ROOT file for the conservative extension of HOL by the LCF logic. |
6 ROOT file for the conservative extension of HOL by the LCF logic. |
7 Should be executed in subdirectory HOLCF. |
7 Should be executed in subdirectory HOLCF. |
8 *) |
8 *) |
9 |
9 |
10 val banner = "Higher-order Logic of Computable Functions; curried version"; |
10 val banner = "HOLCF with sections axioms,ops,domain,generated"; |
|
11 init_thy_reader(); |
|
12 |
|
13 (* start 8bit 1 *) |
|
14 (* end 8bit 1 *) |
|
15 |
11 writeln banner; |
16 writeln banner; |
12 print_depth 1; |
17 print_depth 1; |
13 |
18 |
|
19 use_thy "HOLCF"; |
|
20 |
|
21 (* install sections: axioms, ops *) |
|
22 |
|
23 use "ax_ops/holcflogic.ML"; |
|
24 use "ax_ops/thy_axioms.ML"; |
|
25 use "ax_ops/thy_ops.ML"; |
|
26 use "ax_ops/thy_syntax.ML"; |
|
27 |
|
28 |
|
29 (* install sections: domain, generated *) |
|
30 |
|
31 use "domain/library"; |
|
32 use "domain/syntax"; |
|
33 use "domain/axioms"; |
|
34 use "domain/theorems"; |
|
35 use "domain/extender"; |
|
36 use "domain/interface"; |
|
37 |
14 init_thy_reader(); |
38 init_thy_reader(); |
|
39 init_pps (); |
15 |
40 |
16 use_thy "Fix"; |
41 print_depth 100; |
17 use_thy "Dlist"; |
|
18 |
|
19 use "../Pure/install_pp.ML"; |
|
20 print_depth 8; |
|
21 |
42 |
22 val HOLCF_build_completed = (); (*indicate successful build*) |
43 val HOLCF_build_completed = (); (*indicate successful build*) |