# HG changeset patch
# User wenzelm
# Date 1002202852 -7200
# Node ID c786d9ce558e9b639581aedaacf890fb3e5af6f3
# Parent  abd396ca7ef9bc98de65fcf0d51bfb3a796ebbc0
use "~~/src/Provers/induct_method.ML";

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