--- 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";
--- a/src/FOL/ROOT.ML Mon Nov 03 12:28:14 1997 +0100
+++ b/src/FOL/ROOT.ML Mon Nov 03 12:28:45 1997 +0100
@@ -43,6 +43,9 @@
use_thy "FOL";
+use "cladata.ML";
+use "simpdata.ML";
+
qed_goal "ex1_functional" FOL.thy
"!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"
(fn _ => [ (deepen_tac FOL_cs 0 1) ]);