src/HOL/ROOT.ML
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";