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
     1 (*  Title:      HOLCF/ROOT.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 ROOT file for the conservative extension of HOL by the LCF logic.
     7 Should be executed in subdirectory HOLCF.
     8 *)
     9 
    10 val banner = "HOLCF";
    11 writeln banner;
    12 
    13 set global_names;
    14 
    15 print_depth 1;
    16 
    17 use_thy "HOLCF";
    18 
    19 (* sections axioms, ops *)
    20 
    21 use "ax_ops/holcflogic.ML";
    22 use "ax_ops/thy_axioms.ML";
    23 use "ax_ops/thy_ops.ML";
    24 use "ax_ops/thy_syntax.ML";
    25 
    26 (* sections domain, generated *)
    27 
    28 use "domain/library.ML";
    29 use "domain/syntax.ML";
    30 use "domain/axioms.ML";
    31 use "domain/theorems.ML";
    32 use "domain/extender.ML";
    33 use "domain/interface.ML";
    34 
    35 print_depth 10;  
    36 
    37 val HOLCF_build_completed = (); (*indicate successful build*)