added find_theorems.ML, ../simplifier.ML;
authorwenzelm
Sun, 22 May 2005 16:51:13 +0200
changeset 16025 fa2d7364d359
parent 16024 ffe25459c72a
child 16026 43967e1cba7e
added find_theorems.ML, ../simplifier.ML;
src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Sun May 22 16:51:12 2005 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sun May 22 16:51:13 2005 +0200
@@ -43,5 +43,7 @@
 (*theory and proof operations*)
 use "isar_thy.ML";
 use "constdefs.ML";
+use "../simplifier.ML";
+use "find_theorems.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";