--- a/src/HOLCF/ROOT.ML Thu Jul 14 19:28:22 2005 +0200
+++ b/src/HOLCF/ROOT.ML Thu Jul 14 19:28:23 2005 +0200
@@ -2,23 +2,10 @@
ID: $Id$
Author: Franz Regensburger
-Conservative (semantic) extension of HOL by the LCF logic.
+HOLCF -- a semantic extension of HOL by the LCF logic.
*)
val banner = "HOLCF";
writeln banner;
use_thy "HOLCF";
-
-use "holcf_logic.ML";
-use "cont_consts.ML";
-
-(* domain package *)
-use "domain/library.ML";
-use "domain/syntax.ML";
-use "domain/axioms.ML";
-use "domain/theorems.ML";
-use "domain/extender.ML";
-use "domain/interface.ML";
-
-path_add "~~/src/HOLCF/ex";