src/HOLCF/ROOT.ML
author oheimb
Mon Sep 21 22:58:43 1998 +0200 (1998-09-21)
changeset 5517 863f56450888
parent 4129 2fd816aa6206
child 6349 f7750d816c21
permissions -rw-r--r--
added dependance on HOL
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
oheimb@5517
    10
HOL_build_completed;    (* Cause HOLCF to fail if HOL did *)
oheimb@5517
    11
wenzelm@3623
    12
val banner = "HOLCF";
oheimb@2394
    13
writeln banner;
regensbu@1274
    14
nipkow@243
    15
print_depth 1;
nipkow@243
    16
regensbu@1274
    17
use_thy "HOLCF";
regensbu@1274
    18
wenzelm@4129
    19
use "holcf_logic.ML";
wenzelm@4129
    20
use "cont_consts.ML";
regensbu@1274
    21
oheimb@4122
    22
(* domain package *)
regensbu@1285
    23
use "domain/library.ML";
regensbu@1285
    24
use "domain/syntax.ML";
regensbu@1285
    25
use "domain/axioms.ML";
regensbu@1285
    26
use "domain/theorems.ML";
regensbu@1285
    27
use "domain/extender.ML";
regensbu@1285
    28
use "domain/interface.ML";
nipkow@297
    29
oheimb@2394
    30
print_depth 10;  
oheimb@2394
    31
clasohm@1461
    32
val HOLCF_build_completed = (); (*indicate successful build*)