author | sandnerr |
Mon, 09 Dec 1996 19:07:26 +0100 | |
changeset 2353 | 7405e3cac88a |
parent 2282 | 90fb68d597f8 |
child 2394 | 91d8abf108be |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/ROOT |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
4 |
Copyright 1993 Technische Universitaet Muenchen |
|
243
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 *) |
|
2278 | 14 |
val banner = |
15 |
"HOLCF with sections axioms,ops,domain,generated and 8bit characters"; |
|
1274 | 16 |
(* end 8bit 1 *) |
17 |
||
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
18 |
writeln banner; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
19 |
print_depth 1; |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
20 |
|
1274 | 21 |
use_thy "HOLCF"; |
22 |
||
23 |
(* install sections: axioms, ops *) |
|
24 |
||
25 |
use "ax_ops/holcflogic.ML"; |
|
26 |
use "ax_ops/thy_axioms.ML"; |
|
27 |
use "ax_ops/thy_ops.ML"; |
|
28 |
use "ax_ops/thy_syntax.ML"; |
|
29 |
||
30 |
||
31 |
(* install sections: domain, generated *) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
32 |
|
1285 | 33 |
use "domain/library.ML"; |
34 |
use "domain/syntax.ML"; |
|
35 |
use "domain/axioms.ML"; |
|
36 |
use "domain/theorems.ML"; |
|
37 |
use "domain/extender.ML"; |
|
38 |
use "domain/interface.ML"; |
|
297 | 39 |
|
1274 | 40 |
init_thy_reader(); |
41 |
init_pps (); |
|
42 |
||
43 |
print_depth 100; |
|
1571 | 44 |
make_html:=false; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
45 |
|
2353 | 46 |
fun qed_spec_mp name = |
47 |
let val thm = normalize_thm [RSspec,RSmp] (result()) |
|
48 |
in bind_thm(name, thm) end; |
|
49 |
||
1461 | 50 |
val HOLCF_build_completed = (); (*indicate successful build*) |