--- a/src/HOLCF/ROOT.ML Wed Aug 06 11:57:52 1997 +0200
+++ b/src/HOLCF/ROOT.ML Wed Aug 06 11:58:50 1997 +0200
@@ -1,4 +1,4 @@
-(* Title: HOLCF/ROOT
+(* Title: HOLCF/ROOT.ML
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
@@ -7,14 +7,15 @@
Should be executed in subdirectory HOLCF.
*)
-val banner = "HOLCF with sections axioms,ops,domain,generated";
+val banner = "HOLCF";
writeln banner;
print_depth 1;
use_thy "HOLCF";
-(* install sections: axioms, ops *)
+
+(* sections axioms, ops *)
use "ax_ops/holcflogic.ML";
use "ax_ops/thy_axioms.ML";
@@ -22,7 +23,7 @@
use "ax_ops/thy_syntax.ML";
-(* install sections: domain, generated *)
+(* sections domain, generated *)
use "domain/library.ML";
use "domain/syntax.ML";
@@ -31,11 +32,6 @@
use "domain/extender.ML";
use "domain/interface.ML";
-set_parser ThySyn.parse;
-
-fun qed_spec_mp name =
- let val thm = normalize_thm [RSspec,RSmp] (result())
- in bind_thm(name, thm) end;
print_depth 10;