moved cladata.ML, simpdata.ML to ROOT.ML;
authorwenzelm
Mon Nov 03 12:28:45 1997 +0100 (1997-11-03)
changeset 40968cdf672a83e8
parent 4095 6fd0f439e50e
child 4097 ddd1c18121e0
moved cladata.ML, simpdata.ML to ROOT.ML;
src/FOL/FOL.ML
src/FOL/ROOT.ML
     1.1 --- a/src/FOL/FOL.ML	Mon Nov 03 12:28:14 1997 +0100
     1.2 +++ b/src/FOL/FOL.ML	Mon Nov 03 12:28:45 1997 +0100
     1.3 @@ -70,8 +70,3 @@
     1.4      (REPEAT (DEPTH_SOLVE_1 
     1.5          (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
     1.6  
     1.7 -
     1.8 -(*Thus, assignments to the references claset and simpset are recorded
     1.9 -  with theory "FOL".  These files cannot be loaded directly in ROOT.ML.*)
    1.10 -use "cladata.ML";
    1.11 -use "simpdata.ML";
     2.1 --- a/src/FOL/ROOT.ML	Mon Nov 03 12:28:14 1997 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Mon Nov 03 12:28:45 1997 +0100
     2.3 @@ -43,6 +43,9 @@
     2.4  
     2.5  use_thy "FOL";
     2.6  
     2.7 +use "cladata.ML";
     2.8 +use "simpdata.ML";
     2.9 +
    2.10  qed_goal "ex1_functional" FOL.thy
    2.11      "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
    2.12   (fn _ => [ (deepen_tac FOL_cs 0 1) ]);