| author | wenzelm |
| Sat, 03 Nov 2001 18:41:28 +0100 | |
| changeset 12036 | 49f6c49454c2 |
| parent 6349 | f7750d816c21 |
| child 14535 | 7cb26928e70d |
| permissions | -rw-r--r-- |
| wenzelm@3623 | 1 |
(* Title: HOLCF/ROOT.ML |
| nipkow@243 | 2 |
ID: $Id$ |
| clasohm@1461 | 3 |
Author: Franz Regensburger |
| wenzelm@12036 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
| nipkow@243 | 5 |
|
| wenzelm@12036 | 6 |
Conservative (semantic) extension of HOL by the LCF logic. |
| nipkow@243 | 7 |
*) |
| nipkow@243 | 8 |
|
| wenzelm@3623 | 9 |
val banner = "HOLCF"; |
| oheimb@2394 | 10 |
writeln banner; |
| regensbu@1274 | 11 |
|
| nipkow@243 | 12 |
print_depth 1; |
| nipkow@243 | 13 |
|
| regensbu@1274 | 14 |
use_thy "HOLCF"; |
| regensbu@1274 | 15 |
|
| wenzelm@4129 | 16 |
use "holcf_logic.ML"; |
| wenzelm@4129 | 17 |
use "cont_consts.ML"; |
| regensbu@1274 | 18 |
|
| oheimb@4122 | 19 |
(* domain package *) |
| regensbu@1285 | 20 |
use "domain/library.ML"; |
| regensbu@1285 | 21 |
use "domain/syntax.ML"; |
| regensbu@1285 | 22 |
use "domain/axioms.ML"; |
| regensbu@1285 | 23 |
use "domain/theorems.ML"; |
| regensbu@1285 | 24 |
use "domain/extender.ML"; |
| regensbu@1285 | 25 |
use "domain/interface.ML"; |
| regensbu@1274 | 26 |
|
| oheimb@2394 | 27 |
print_depth 10; |