simplified EqSubst setup;
authorwenzelm
Fri Jan 06 18:18:13 2006 +0100 (2006-01-06)
changeset 18595a52907967bae
parent 18594 e0d509b1df1d
child 18596 1e876583e247
simplified EqSubst setup;
src/FOL/FOL.thy
src/FOL/ROOT.ML
src/HOL/HOL.thy
src/HOL/ROOT.ML
     1.1 --- a/src/FOL/FOL.thy	Fri Jan 06 18:18:12 2006 +0100
     1.2 +++ b/src/FOL/FOL.thy	Fri Jan 06 18:18:13 2006 +0100
     1.3 @@ -8,8 +8,6 @@
     1.4  theory FOL
     1.5  imports IFOL
     1.6  uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
     1.7 -      ("eqrule_FOL_data.ML")
     1.8 -      ("~~/src/Provers/eqsubst.ML")
     1.9  begin
    1.10  
    1.11  
    1.12 @@ -45,13 +43,6 @@
    1.13  setup "Simplifier.method_setup Splitter.split_modifiers"
    1.14  setup Splitter.setup
    1.15  setup Clasimp.setup
    1.16 -
    1.17 -
    1.18 -subsection {* Lucas Dixon's eqstep tactic *}
    1.19 -
    1.20 -use "~~/src/Provers/eqsubst.ML";
    1.21 -use "eqrule_FOL_data.ML";
    1.22 -
    1.23  setup EqSubst.setup
    1.24  
    1.25  
     2.1 --- a/src/FOL/ROOT.ML	Fri Jan 06 18:18:12 2006 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Fri Jan 06 18:18:13 2006 +0100
     2.3 @@ -11,6 +11,7 @@
     2.4  use "~~/src/Provers/splitter.ML";
     2.5  use "~~/src/Provers/ind.ML";
     2.6  use "~~/src/Provers/hypsubst.ML";
     2.7 +use "~~/src/Provers/eqsubst.ML";
     2.8  use "~~/src/Provers/induct_method.ML";
     2.9  use "~~/src/Provers/classical.ML";
    2.10  use "~~/src/Provers/blast.ML";
     3.1 --- a/src/HOL/HOL.thy	Fri Jan 06 18:18:12 2006 +0100
     3.2 +++ b/src/HOL/HOL.thy	Fri Jan 06 18:18:13 2006 +0100
     3.3 @@ -7,8 +7,7 @@
     3.4  
     3.5  theory HOL
     3.6  imports CPure
     3.7 -uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML")
     3.8 -      ("~~/src/Provers/eqsubst.ML")
     3.9 +uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML")
    3.10  
    3.11  begin
    3.12  
    3.13 @@ -1188,12 +1187,6 @@
    3.14  use "simpdata.ML"
    3.15  setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    3.16  setup Splitter.setup setup Clasimp.setup
    3.17 -
    3.18 -
    3.19 -text {* \medskip Lucas Dixon's eqstep tactic. *}
    3.20 -
    3.21 -use "~~/src/Provers/eqsubst.ML";
    3.22 -use "eqrule_HOL_data.ML";
    3.23  setup EqSubst.setup
    3.24  
    3.25  
     4.1 --- a/src/HOL/ROOT.ML	Fri Jan 06 18:18:12 2006 +0100
     4.2 +++ b/src/HOL/ROOT.ML	Fri Jan 06 18:18:13 2006 +0100
     4.3 @@ -13,6 +13,7 @@
     4.4  
     4.5  use "~~/src/Provers/splitter.ML";
     4.6  use "~~/src/Provers/hypsubst.ML";
     4.7 +use "~~/src/Provers/eqsubst.ML";
     4.8  use "~~/src/Provers/induct_method.ML";
     4.9  use "~~/src/Provers/classical.ML";
    4.10  use "~~/src/Provers/blast.ML";