src/HOLCF/ROOT.ML
author oheimb
Mon Oct 27 11:34:33 1997 +0100 (1997-10-27)
changeset 4008 2444085532c6
parent 3953 473ea5ce5ca8
child 4010 59cac65fb751
permissions -rw-r--r--
adapted domain and ax_ops package for name spaces
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
wenzelm@3953
    13
set global_names;
wenzelm@3953
    14
nipkow@243
    15
print_depth 1;
nipkow@243
    16
regensbu@1274
    17
use_thy "HOLCF";
regensbu@1274
    18
wenzelm@3623
    19
(* sections axioms, ops *)
regensbu@1274
    20
regensbu@1274
    21
use "ax_ops/holcflogic.ML";
regensbu@1274
    22
use "ax_ops/thy_axioms.ML";
regensbu@1274
    23
use "ax_ops/thy_ops.ML";
regensbu@1274
    24
use "ax_ops/thy_syntax.ML";
regensbu@1274
    25
wenzelm@3623
    26
(* sections domain, generated *)
nipkow@243
    27
regensbu@1285
    28
use "domain/library.ML";
regensbu@1285
    29
use "domain/syntax.ML";
regensbu@1285
    30
use "domain/axioms.ML";
regensbu@1285
    31
use "domain/theorems.ML";
regensbu@1285
    32
use "domain/extender.ML";
regensbu@1285
    33
use "domain/interface.ML";
nipkow@297
    34
oheimb@2394
    35
print_depth 10;  
oheimb@2394
    36
clasohm@1461
    37
val HOLCF_build_completed = (); (*indicate successful build*)