--- a/src/Provers/README Mon Dec 13 18:18:34 1993 +0100
+++ b/src/Provers/README Mon Dec 13 18:48:47 1993 +0100
@@ -2,11 +2,14 @@
This directory contains ML sources of generic theorem proving tools.
Typically, they can be applied to various logics, provided rules of a
-certain form are derivable. Unfortunately, little documentation is
-available.
+certain form are derivable. The first three are documented in the
+Reference Manual.
-classical.ML -- theorem prover for classical logics
-genelim.ML -- bits and pieces for deriving elimination rules
-ind.ML -- a simple induction package
-simp.ML -- a powerful simplifier
-typedsimp.ML -- a rather basic simplifier for explicitly typed logics
+classical.ML -- theorem prover for classical logics
+hypsubst.ML -- tactic to substitute in the hypotheses
+simplifier.ML -- fast simplifier
+simp.ML -- powerful but slow simplifier
+typedsimp.ML -- basic simplifier for explicitly typed logics
+splitter.ML -- performs case splits for simplifier.ML
+genelim.ML -- bits and pieces for deriving elimination rules
+ind.ML -- a simple induction package