# HG changeset patch
# User wenzelm
# Date 887294630 -3600
# Node ID e6ada440a383ada701ee54c49cc3e2a9448f1647
# Parent  85aae356570c7eea90068829d117e7761f7fff1a
updated;

diff -r 85aae356570c -r e6ada440a383 src/Provers/README
--- a/src/Provers/README	Thu Feb 12 15:00:04 1998 +0100
+++ b/src/Provers/README	Thu Feb 12 15:43:50 1998 +0100
@@ -1,23 +1,22 @@
-
-                        Provers
+                 Provers: generic theorem proving tools
 
 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.  Some of these are documented in the
 Reference Manual.
 
-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
-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
+  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
+  quantifier1.ML	simplification procedures for "1 point rules"
+  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
 
 directory Arith:
-  nat_transitive.ML     -- simple package for inequalities over nat
-
-
-$Id$
+  cancel_factor.ML	cancel common constant factor
+  cancel_sums.ML	cancel common summands
+  nat_transitive.ML	simple package for inequalities over nat