--- a/src/HOLCF/ROOT.ML Fri Dec 13 18:40:50 1996 +0100
+++ b/src/HOLCF/ROOT.ML Fri Dec 13 18:45:58 1996 +0100
@@ -8,14 +8,8 @@
*)
val banner = "HOLCF with sections axioms,ops,domain,generated";
-init_thy_reader();
+writeln banner;
-(* start 8bit 1 *)
-val banner =
- "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
-(* end 8bit 1 *)
-
-writeln banner;
print_depth 1;
use_thy "HOLCF";
@@ -40,11 +34,10 @@
init_thy_reader();
init_pps ();
-print_depth 100;
-make_html:=false;
-
fun qed_spec_mp name =
let val thm = normalize_thm [RSspec,RSmp] (result())
in bind_thm(name, thm) end;
+print_depth 10;
+
val HOLCF_build_completed = (); (*indicate successful build*)