author wenzelm Thu, 12 Feb 1998 15:43:50 +0100 changeset 4623 e6ada440a383 parent 4622 85aae356570c child 4624 795b5b624c02
updated;
 src/Provers/README file | annotate | diff | comparison | revisions
```--- 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```