# HG changeset patch
# User wenzelm
# Date 1003521745 -7200
# Node ID 54fe56353704cb094717b6ff773789ab4bcb4492
# Parent  3ef83c265acad5bbf292152e5720503bbe3062f7
induct_method.ML -- proof by cases and induction on sets and types (Isar);

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