use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML;

--- a/src/HOL/HOL.ML	Mon Nov 03 12:09:37 1997 +0100
+++ b/src/HOL/HOL.ML	Mon Nov 03 12:11:34 1997 +0100
@@ -374,10 +374,3 @@
 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
 
 end;
-
-
-(*Thus, assignments to the references claset and simpset are recorded
-  with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)
-use "hologic.ML";
-use "cladata.ML";
-use "simpdata.ML";