src/HOLCF/ROOT.ML

--- a/src/HOLCF/ROOT.ML	Fri Oct 06 16:17:08 1995 +0100
+++ b/src/HOLCF/ROOT.ML	Fri Oct 06 17:25:24 1995 +0100
@@ -7,16 +7,37 @@
 Should be executed in subdirectory HOLCF.
 *)
 
-val banner = "Higher-order Logic of Computable Functions; curried version";
+val banner = "HOLCF with sections axioms,ops,domain,generated";
+init_thy_reader();
+
+(* start 8bit 1 *)
+(* end 8bit 1 *)
+
 writeln banner;
 print_depth 1;
 
-init_thy_reader();
+use_thy "HOLCF";
+
+(* install sections: axioms, ops *)
+
+use "ax_ops/holcflogic.ML";
+use "ax_ops/thy_axioms.ML";
+use "ax_ops/thy_ops.ML";
+use "ax_ops/thy_syntax.ML";
+
+
+(* install sections: domain, generated *)
 
-use_thy "Fix";
-use_thy "Dlist";
+use "domain/library";
+use "domain/syntax";
+use "domain/axioms";
+use "domain/theorems";
+use "domain/extender";
+use "domain/interface";
 
-use "../Pure/install_pp.ML";
-print_depth 8;  
+init_thy_reader();
+init_pps ();
+
+print_depth 100;  
 
 val HOLCF_build_completed = ();	(*indicate successful build*)