author | wenzelm |
Wed, 09 Jul 1997 17:00:34 +0200 | |
changeset 3511 | da4dd8b7ced4 |
parent 2394 | 91d8abf108be |
child 3608 | d81caea336ba |
permissions | -rw-r--r-- |
clasohm@1461 | 1 |
(* Title: HOLCF/ROOT |
nipkow@243 | 2 |
ID: $Id$ |
clasohm@1461 | 3 |
Author: Franz Regensburger |
clasohm@1461 | 4 |
Copyright 1993 Technische Universitaet Muenchen |
nipkow@243 | 5 |
|
nipkow@243 | 6 |
ROOT file for the conservative extension of HOL by the LCF logic. |
nipkow@243 | 7 |
Should be executed in subdirectory HOLCF. |
nipkow@243 | 8 |
*) |
nipkow@243 | 9 |
|
regensbu@1274 | 10 |
val banner = "HOLCF with sections axioms,ops,domain,generated"; |
oheimb@2394 | 11 |
writeln banner; |
regensbu@1274 | 12 |
|
nipkow@243 | 13 |
print_depth 1; |
nipkow@243 | 14 |
|
regensbu@1274 | 15 |
use_thy "HOLCF"; |
regensbu@1274 | 16 |
|
regensbu@1274 | 17 |
(* install sections: axioms, ops *) |
regensbu@1274 | 18 |
|
regensbu@1274 | 19 |
use "ax_ops/holcflogic.ML"; |
regensbu@1274 | 20 |
use "ax_ops/thy_axioms.ML"; |
regensbu@1274 | 21 |
use "ax_ops/thy_ops.ML"; |
regensbu@1274 | 22 |
use "ax_ops/thy_syntax.ML"; |
regensbu@1274 | 23 |
|
regensbu@1274 | 24 |
|
regensbu@1274 | 25 |
(* install sections: domain, generated *) |
regensbu@1274 | 26 |
|
regensbu@1285 | 27 |
use "domain/library.ML"; |
regensbu@1285 | 28 |
use "domain/syntax.ML"; |
regensbu@1285 | 29 |
use "domain/axioms.ML"; |
regensbu@1285 | 30 |
use "domain/theorems.ML"; |
regensbu@1285 | 31 |
use "domain/extender.ML"; |
regensbu@1285 | 32 |
use "domain/interface.ML"; |
regensbu@1274 | 33 |
|
wenzelm@393 | 34 |
init_thy_reader(); |
nipkow@243 | 35 |
|
sandnerr@2353 | 36 |
fun qed_spec_mp name = |
sandnerr@2353 | 37 |
let val thm = normalize_thm [RSspec,RSmp] (result()) |
sandnerr@2353 | 38 |
in bind_thm(name, thm) end; |
sandnerr@2353 | 39 |
|
oheimb@2394 | 40 |
print_depth 10; |
oheimb@2394 | 41 |
|
clasohm@1461 | 42 |
val HOLCF_build_completed = (); (*indicate successful build*) |