src/HOLCF/ROOT.ML
author clasohm
Tue Nov 21 15:10:12 1995 +0100 (1995-11-21)
changeset 1361 90d615b599d9
parent 1307 63a5788774f7
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
main directory is now read by exit_use_dir, too;
removed make_chart from ROOT.ML
     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 (* end 8bit 1 *)
    15 
    16 writeln banner;
    17 print_depth 1;
    18 
    19 use_thy "HOLCF";
    20 
    21 (* install sections: axioms, ops *)
    22 
    23 use "ax_ops/holcflogic.ML";
    24 use "ax_ops/thy_axioms.ML";
    25 use "ax_ops/thy_ops.ML";
    26 use "ax_ops/thy_syntax.ML";
    27 
    28 
    29 (* install sections: domain, generated *)
    30 
    31 use "domain/library.ML";
    32 use "domain/syntax.ML";
    33 use "domain/axioms.ML";
    34 use "domain/theorems.ML";
    35 use "domain/extender.ML";
    36 use "domain/interface.ML";
    37 
    38 init_thy_reader();
    39 init_pps ();
    40 
    41 print_depth 100;  
    42 
    43 val HOLCF_build_completed = ();	(*indicate successful build*)