# HG changeset patch
# User wenzelm
# Date 1136567893 -3600
# Node ID a52907967bae489b8ca73ebc23871beb8216ab1c
# Parent  e0d509b1df1dd6576c2277f301870f11a8506d19
simplified EqSubst setup;

diff -r e0d509b1df1d -r a52907967bae src/FOL/FOL.thy
--- 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
 
 
diff -r e0d509b1df1d -r a52907967bae src/FOL/ROOT.ML
--- 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";
diff -r e0d509b1df1d -r a52907967bae src/HOL/HOL.thy
--- 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
 
 
diff -r e0d509b1df1d -r a52907967bae src/HOL/ROOT.ML
--- 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";