src/HOLCF/ROOT.ML
author regensbu
Tue Oct 17 17:00:10 1995 +0100 (1995-10-17)
changeset 1285 4dd0651d692d
parent 1274 ea0668a1c0ba
child 1307 63a5788774f7
permissions -rw-r--r--
removed incompatibility with sml
nipkow@243
     1
(*  Title:	HOLCF/ROOT
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     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
regensbu@1274
    10
val banner = "HOLCF with sections axioms,ops,domain,generated";
regensbu@1274
    11
init_thy_reader();
regensbu@1274
    12
regensbu@1274
    13
(* start 8bit 1 *)
regensbu@1274
    14
(* end 8bit 1 *)
regensbu@1274
    15
nipkow@243
    16
writeln banner;
nipkow@243
    17
print_depth 1;
nipkow@243
    18
regensbu@1274
    19
use_thy "HOLCF";
regensbu@1274
    20
regensbu@1274
    21
(* install sections: axioms, ops *)
regensbu@1274
    22
regensbu@1274
    23
use "ax_ops/holcflogic.ML";
regensbu@1274
    24
use "ax_ops/thy_axioms.ML";
regensbu@1274
    25
use "ax_ops/thy_ops.ML";
regensbu@1274
    26
use "ax_ops/thy_syntax.ML";
regensbu@1274
    27
regensbu@1274
    28
regensbu@1274
    29
(* install sections: domain, generated *)
nipkow@243
    30
regensbu@1285
    31
use "domain/library.ML";
regensbu@1285
    32
use "domain/syntax.ML";
regensbu@1285
    33
use "domain/axioms.ML";
regensbu@1285
    34
use "domain/theorems.ML";
regensbu@1285
    35
use "domain/extender.ML";
regensbu@1285
    36
use "domain/interface.ML";
nipkow@297
    37
regensbu@1274
    38
init_thy_reader();
regensbu@1274
    39
init_pps ();
regensbu@1274
    40
regensbu@1274
    41
print_depth 100;  
nipkow@243
    42
nipkow@243
    43
val HOLCF_build_completed = ();	(*indicate successful build*)