Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Provers/README
changeset 11840 54fe56353704
parent 8870 e900a58cafe4
child 13735 7de9342aca7a 
--- 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
isabelle