src/HOLCF/ROOT.ML
author wenzelm
Tue Nov 04 16:57:52 1997 +0100 (1997-11-04)
changeset 4128 42584a53a3e7
parent 4122 f63c283cefaf
child 4129 2fd816aa6206
permissions -rw-r--r--
tuned to make non-Poly/MLs happy;
wenzelm@3623
     1
(*  Title:      HOLCF/ROOT.ML
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
wenzelm@3623
    10
val banner = "HOLCF";
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
wenzelm@4128
    17
use "HOLCFLogic.ML";
wenzelm@4128
    18
use "contconsts.ML";
regensbu@1274
    19
oheimb@4122
    20
(* domain package *)
regensbu@1285
    21
use "domain/library.ML";
regensbu@1285
    22
use "domain/syntax.ML";
regensbu@1285
    23
use "domain/axioms.ML";
regensbu@1285
    24
use "domain/theorems.ML";
regensbu@1285
    25
use "domain/extender.ML";
regensbu@1285
    26
use "domain/interface.ML";
nipkow@297
    27
oheimb@2394
    28
print_depth 10;  
oheimb@2394
    29
clasohm@1461
    30
val HOLCF_build_completed = (); (*indicate successful build*)