changeset 3578 | b2b9a9ddb9cc |
parent 3511 | da4dd8b7ced4 |
child 3947 | eb707467f8c5 |
--- a/src/HOL/ROOT.ML Fri Jul 25 13:18:09 1997 +0200 +++ b/src/HOL/ROOT.ML Fri Jul 25 13:18:45 1997 +0200 @@ -16,6 +16,7 @@ use "../Pure/section_utils.ML"; use "thy_syntax.ML"; +use "../Provers/simplifier.ML"; use "../Provers/splitter.ML"; use "../Provers/hypsubst.ML"; use "../Provers/classical.ML";