src/FOL/FOL.ML
changeset 4096 8cdf672a83e8
parent 3835 9a5a4e123859
child 4186 e39f28f94cf8
--- a/src/FOL/FOL.ML	Mon Nov 03 12:28:14 1997 +0100
+++ b/src/FOL/FOL.ML	Mon Nov 03 12:28:45 1997 +0100
@@ -70,8 +70,3 @@
     (REPEAT (DEPTH_SOLVE_1 
         (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
 
-
-(*Thus, assignments to the references claset and simpset are recorded
-  with theory "FOL".  These files cannot be loaded directly in ROOT.ML.*)
-use "cladata.ML";
-use "simpdata.ML";