induct_method.ML -- proof by cases and induction on sets and types (Isar);
authorwenzelm
Fri, 19 Oct 2001 22:02:25 +0200
changeset 11840 54fe56353704
parent 11839 3ef83c265aca
child 11841 ec105d09fc1f
induct_method.ML -- proof by cases and induction on sets and types (Isar);
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