changeset 18595 | a52907967bae |
parent 18529 | 540da2415751 |
child 19161 | b395f586633f |
--- 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";