added clasimp.ML;
authorwenzelm
Thu, 26 Feb 1998 10:41:36 +0100
changeset 4654 dbeae12ada20
parent 4653 d60f76680bf4
child 4655 481628ea8edd
added clasimp.ML;
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