changeset 2469 | b50b8c0eec01 |
parent 1459 | d12da312eff4 |
child 2576 | 390c9fb786b5 |
--- a/src/FOL/FOL.ML Fri Jan 03 10:48:28 1997 +0100 +++ b/src/FOL/FOL.ML Fri Jan 03 15:01:55 1997 +0100 @@ -67,3 +67,9 @@ [ (rtac conjE 1), (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";