src/FOL/FOL.ML
changeset 2469 b50b8c0eec01
parent 1459 d12da312eff4
child 2576 390c9fb786b5
     1.1 --- a/src/FOL/FOL.ML	Fri Jan 03 10:48:28 1997 +0100
     1.2 +++ b/src/FOL/FOL.ML	Fri Jan 03 15:01:55 1997 +0100
     1.3 @@ -67,3 +67,9 @@
     1.4    [ (rtac conjE 1),
     1.5      (REPEAT (DEPTH_SOLVE_1 
     1.6          (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
     1.7 +
     1.8 +
     1.9 +(*Thus, assignments to the references claset and simpset are recorded
    1.10 +  with theory "FOL".  These files cannot be loaded directly in ROOT.ML.*)
    1.11 +use "cladata.ML";
    1.12 +use "simpdata.ML";