diff -r 3ef83c265aca -r 54fe56353704 src/Provers/README
--- a/src/Provers/README	Fri Oct 19 22:02:02 2001 +0200
+++ b/src/Provers/README	Fri Oct 19 22:02:25 2001 +0200
@@ -10,6 +10,7 @@
   classical.ML          theorem prover for classical logics
   hypsubst.ML           tactic to substitute in the hypotheses
   ind.ML                a simple induction package
+  induct_method.ML      proof by cases and induction on sets and types (Isar)
   quantifier1.ML	simplification procedures for "1 point rules"
   simp.ML               powerful but slow simplifier
   simplifier.ML         fast simplifier