# HG changeset patch
# User wenzelm
# Date 888486096 -3600
# Node ID dbeae12ada2072313f4b7975aa8bbe58bdbb2f89
# Parent  d60f76680bf4fdaa9cd1a074f15bef61e41e07a8
added clasimp.ML;

diff -r d60f76680bf4 -r dbeae12ada20 src/Provers/README
--- a/src/Provers/README	Wed Feb 25 20:29:58 1998 +0100
+++ b/src/Provers/README	Thu Feb 26 10:41:36 1998 +0100
@@ -6,6 +6,7 @@
 Reference Manual.
 
   blast.ML              generic tableau prover with proof reconstruction
+  clasimp.ML		combination of classical reasoner and simplifier
   classical.ML          theorem prover for classical logics
   genelim.ML            bits and pieces for deriving elimination rules
   hypsubst.ML           tactic to substitute in the hypotheses