--- 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