src/HOLCF/ROOT.ML
author oheimb
Fri Nov 29 12:22:22 1996 +0100 (1996-11-29)
changeset 2278 d63ffafce255
parent 2275 dbce3dce821a
child 2282 90fb68d597f8
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      HOLCF/ROOT
     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 with sections axioms,ops,domain,generated";
    11 init_thy_reader();
    12 
    13 (* start 8bit 1 *)
    14 val banner = 
    15         "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
    16 (* end 8bit 1 *)
    17 
    18 writeln banner;
    19 print_depth 1;
    20 
    21 use_thy "HOLCF";
    22 
    23 (* install sections: axioms, ops *)
    24 
    25 use "ax_ops/holcflogic.ML";
    26 use "ax_ops/thy_axioms.ML";
    27 use "ax_ops/thy_ops.ML";
    28 use "ax_ops/thy_syntax.ML";
    29 
    30 
    31 (* install sections: domain, generated *)
    32 
    33 use "domain/library.ML";
    34 use "domain/syntax.ML";
    35 use "domain/axioms.ML";
    36 use "domain/theorems.ML";
    37 use "domain/extender.ML";
    38 use "domain/interface.ML";
    39 
    40 init_thy_reader();
    41 init_pps ();
    42 
    43 print_depth 100;  
    44 make_html:=false;
    45 
    46 val HOLCF_build_completed = (); (*indicate successful build*)