src/HOLCF/ROOT.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5517 863f56450888
child 12036 49f6c49454c2
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
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@4129
    17
use "holcf_logic.ML";
wenzelm@4129
    18
use "cont_consts.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;