src/HOLCF/ROOT.ML
changeset 4122 f63c283cefaf
parent 4041 4df7f385fe9f
child 4128 42584a53a3e7
--- a/src/HOLCF/ROOT.ML	Tue Nov 04 14:37:51 1997 +0100
+++ b/src/HOLCF/ROOT.ML	Tue Nov 04 14:40:29 1997 +0100
@@ -14,14 +14,10 @@
 
 use_thy "HOLCF";
 
-(* 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";
+use "HOLCFLogic";
+use "contconsts";
 
-(* sections domain, generated *)
-
+(* domain package *)
 use "domain/library.ML";
 use "domain/syntax.ML";
 use "domain/axioms.ML";