--- a/src/FOL/FOL.thy Fri Jan 06 18:18:12 2006 +0100
+++ b/src/FOL/FOL.thy Fri Jan 06 18:18:13 2006 +0100
@@ -8,8 +8,6 @@
theory FOL
imports IFOL
uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
- ("eqrule_FOL_data.ML")
- ("~~/src/Provers/eqsubst.ML")
begin
@@ -45,13 +43,6 @@
setup "Simplifier.method_setup Splitter.split_modifiers"
setup Splitter.setup
setup Clasimp.setup
-
-
-subsection {* Lucas Dixon's eqstep tactic *}
-
-use "~~/src/Provers/eqsubst.ML";
-use "eqrule_FOL_data.ML";
-
setup EqSubst.setup