diff -r 6fd0f439e50e -r 8cdf672a83e8 src/FOL/FOL.ML --- 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";