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