--- a/src/FOL/FOL.thy Sun Jan 30 20:48:50 2005 +0100
+++ b/src/FOL/FOL.thy Tue Feb 01 18:01:57 2005 +0100
@@ -5,9 +5,12 @@
header {* Classical first-order logic *}
-theory FOL = IFOL
-files
- ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"):
+theory FOL
+imports IFOL
+files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
+ ("eqrule_FOL_data.ML")
+ ("~~/src/Provers/eqsubst.ML")
+begin
subsection {* The classical axiom *}
@@ -43,6 +46,15 @@
setup Splitter.setup
setup Clasimp.setup
+
+subsection {* Lucas Dixon's eqstep tactic *}
+
+use "~~/src/Provers/eqsubst.ML";
+use "eqrule_FOL_data.ML";
+
+setup EQSubstTac.setup
+
+
subsection {* Other simple lemmas *}
lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)"