src/HOLCF/ROOT.ML
changeset 1274 ea0668a1c0ba
parent 1267 bca91b4e1710
child 1285 4dd0651d692d
     1.1 --- a/src/HOLCF/ROOT.ML	Fri Oct 06 16:17:08 1995 +0100
     1.2 +++ b/src/HOLCF/ROOT.ML	Fri Oct 06 17:25:24 1995 +0100
     1.3 @@ -7,16 +7,37 @@
     1.4  Should be executed in subdirectory HOLCF.
     1.5  *)
     1.6  
     1.7 -val banner = "Higher-order Logic of Computable Functions; curried version";
     1.8 +val banner = "HOLCF with sections axioms,ops,domain,generated";
     1.9 +init_thy_reader();
    1.10 +
    1.11 +(* start 8bit 1 *)
    1.12 +(* end 8bit 1 *)
    1.13 +
    1.14  writeln banner;
    1.15  print_depth 1;
    1.16  
    1.17 -init_thy_reader();
    1.18 +use_thy "HOLCF";
    1.19 +
    1.20 +(* install sections: axioms, ops *)
    1.21 +
    1.22 +use "ax_ops/holcflogic.ML";
    1.23 +use "ax_ops/thy_axioms.ML";
    1.24 +use "ax_ops/thy_ops.ML";
    1.25 +use "ax_ops/thy_syntax.ML";
    1.26 +
    1.27 +
    1.28 +(* install sections: domain, generated *)
    1.29  
    1.30 -use_thy "Fix";
    1.31 -use_thy "Dlist";
    1.32 +use "domain/library";
    1.33 +use "domain/syntax";
    1.34 +use "domain/axioms";
    1.35 +use "domain/theorems";
    1.36 +use "domain/extender";
    1.37 +use "domain/interface";
    1.38  
    1.39 -use "../Pure/install_pp.ML";
    1.40 -print_depth 8;  
    1.41 +init_thy_reader();
    1.42 +init_pps ();
    1.43 +
    1.44 +print_depth 100;  
    1.45  
    1.46  val HOLCF_build_completed = ();	(*indicate successful build*)