--- 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
--- a/src/FOL/ROOT.ML Fri Jan 06 18:18:12 2006 +0100
+++ b/src/FOL/ROOT.ML Fri Jan 06 18:18:13 2006 +0100
@@ -11,6 +11,7 @@
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/ind.ML";
use "~~/src/Provers/hypsubst.ML";
+use "~~/src/Provers/eqsubst.ML";
use "~~/src/Provers/induct_method.ML";
use "~~/src/Provers/classical.ML";
use "~~/src/Provers/blast.ML";
--- a/src/HOL/HOL.thy Fri Jan 06 18:18:12 2006 +0100
+++ b/src/HOL/HOL.thy Fri Jan 06 18:18:13 2006 +0100
@@ -7,8 +7,7 @@
theory HOL
imports CPure
-uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML")
- ("~~/src/Provers/eqsubst.ML")
+uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
begin
@@ -1188,12 +1187,6 @@
use "simpdata.ML"
setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
setup Splitter.setup setup Clasimp.setup
-
-
-text {* \medskip Lucas Dixon's eqstep tactic. *}
-
-use "~~/src/Provers/eqsubst.ML";
-use "eqrule_HOL_data.ML";
setup EqSubst.setup
--- a/src/HOL/ROOT.ML Fri Jan 06 18:18:12 2006 +0100
+++ b/src/HOL/ROOT.ML Fri Jan 06 18:18:13 2006 +0100
@@ -13,6 +13,7 @@
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/hypsubst.ML";
+use "~~/src/Provers/eqsubst.ML";
use "~~/src/Provers/induct_method.ML";
use "~~/src/Provers/classical.ML";
use "~~/src/Provers/blast.ML";