use "~~/src/Provers/induct_method.ML";
authorwenzelm
Thu Oct 04 15:40:52 2001 +0200 (2001-10-04)
changeset 11685c786d9ce558e
parent 11684 abd396ca7ef9
child 11686 68b95cb97745
use "~~/src/Provers/induct_method.ML";
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/ROOT.ML	Thu Oct 04 15:40:31 2001 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Thu Oct 04 15:40:52 2001 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4  use "~~/src/Provers/splitter.ML";
     1.5  use "~~/src/Provers/hypsubst.ML";
     1.6  use "~~/src/Provers/rulify.ML";
     1.7 +use "~~/src/Provers/induct_method.ML";
     1.8  use "~~/src/Provers/make_elim.ML";
     1.9  use "~~/src/Provers/classical.ML";
    1.10  use "~~/src/Provers/blast.ML";