--- a/src/HOLCF/ROOT.ML Mon Dec 09 16:51:14 1996 +0100
+++ b/src/HOLCF/ROOT.ML Mon Dec 09 19:07:26 1996 +0100
@@ -10,10 +10,6 @@
val banner = "HOLCF with sections axioms,ops,domain,generated";
init_thy_reader();
-fun qed_spec_mp name =
- let val thm = normalize_thm [RSspec,RSmp] (result())
- in bind_thm(name, thm) end;
-
(* start 8bit 1 *)
val banner =
"HOLCF with sections axioms,ops,domain,generated and 8bit characters";
@@ -47,4 +43,8 @@
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;
+
val HOLCF_build_completed = (); (*indicate successful build*)