# HG changeset patch
# User lcp
# Date 755804927 -3600
# Node ID 1315ce07f5156e941d89e236bdd327b2ade82005
# Parent  06e31ac55dd1b6e9c2bb64b272911979c0802f8e
added mention of simplifier, splitter, hypsubst

diff -r 06e31ac55dd1 -r 1315ce07f515 src/Provers/README
--- 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