author | regensbu |
Tue, 17 Oct 1995 17:00:10 +0100 | |
changeset 1285 | 4dd0651d692d |
parent 1274 | ea0668a1c0ba |
child 1307 | 63a5788774f7 |
permissions | -rw-r--r-- |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOLCF/ROOT |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
Author: Franz Regensburger |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
ROOT file for the conservative extension of HOL by the LCF logic. |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
Should be executed in subdirectory HOLCF. |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
|
1274 | 10 |
val banner = "HOLCF with sections axioms,ops,domain,generated"; |
11 |
init_thy_reader(); |
|
12 |
||
13 |
(* start 8bit 1 *) |
|
14 |
(* end 8bit 1 *) |
|
15 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
writeln banner; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
17 |
print_depth 1; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
|
1274 | 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 *) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
30 |
|
1285 | 31 |
use "domain/library.ML"; |
32 |
use "domain/syntax.ML"; |
|
33 |
use "domain/axioms.ML"; |
|
34 |
use "domain/theorems.ML"; |
|
35 |
use "domain/extender.ML"; |
|
36 |
use "domain/interface.ML"; |
|
297 | 37 |
|
1274 | 38 |
init_thy_reader(); |
39 |
init_pps (); |
|
40 |
||
41 |
print_depth 100; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
42 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
43 |
val HOLCF_build_completed = (); (*indicate successful build*) |