diff -r 636322bfd057 -r 815ef5848324 src/Provers/README
--- a/src/Provers/README	Wed May 21 17:11:46 1997 +0200
+++ b/src/Provers/README	Wed May 21 17:13:00 1997 +0200
@@ -2,14 +2,16 @@
 
 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.  The first three are documented in the
+certain form are derivable.  Some of these are documented in the
 Reference Manual.
 
-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
+blast.ML          -- generic tableau prover with proof reconstruction
+classical.ML      -- theorem prover for classical logics
+genelim.ML        -- bits and pieces for deriving elimination rules
+hypsubst.ML       -- tactic to substitute in the hypotheses
+ind.ML            -- a simple induction package
+nat_transitive.ML -- simple package for inequalities over nat
+simp.ML           -- powerful but slow simplifier
+simplifier.ML     -- fast simplifier
+splitter.ML       -- performs case splits for simplifier.ML
+typedsimp.ML      -- basic simplifier for explicitly typed logics