src/HOL/ROOT.ML
changeset 11685 c786d9ce558e
parent 10766 ace2ba2d4fd1
child 11770 b6bb7a853dd2
--- a/src/HOL/ROOT.ML	Thu Oct 04 15:40:31 2001 +0200
+++ b/src/HOL/ROOT.ML	Thu Oct 04 15:40:52 2001 +0200
@@ -21,6 +21,7 @@
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/hypsubst.ML";
 use "~~/src/Provers/rulify.ML";
+use "~~/src/Provers/induct_method.ML";
 use "~~/src/Provers/make_elim.ML";
 use "~~/src/Provers/classical.ML";
 use "~~/src/Provers/blast.ML";