updated;
authorwenzelm
Thu Feb 12 15:43:50 1998 +0100 (1998-02-12)
changeset 4623e6ada440a383
parent 4622 85aae356570c
child 4624 795b5b624c02
updated;
src/Provers/README
     1.1 --- a/src/Provers/README	Thu Feb 12 15:00:04 1998 +0100
     1.2 +++ b/src/Provers/README	Thu Feb 12 15:43:50 1998 +0100
     1.3 @@ -1,23 +1,22 @@
     1.4 -
     1.5 -                        Provers
     1.6 +                 Provers: generic theorem proving tools
     1.7  
     1.8  This directory contains ML sources of generic theorem proving tools.
     1.9  Typically, they can be applied to various logics, provided rules of a
    1.10  certain form are derivable.  Some of these are documented in the
    1.11  Reference Manual.
    1.12  
    1.13 -blast.ML                -- generic tableau prover with proof reconstruction
    1.14 -classical.ML            -- theorem prover for classical logics
    1.15 -genelim.ML              -- bits and pieces for deriving elimination rules
    1.16 -hypsubst.ML             -- tactic to substitute in the hypotheses
    1.17 -ind.ML                  -- a simple induction package
    1.18 -simp.ML                 -- powerful but slow simplifier
    1.19 -simplifier.ML           -- fast simplifier
    1.20 -splitter.ML             -- performs case splits for simplifier.ML
    1.21 -typedsimp.ML            -- basic simplifier for explicitly typed logics
    1.22 +  blast.ML              generic tableau prover with proof reconstruction
    1.23 +  classical.ML          theorem prover for classical logics
    1.24 +  genelim.ML            bits and pieces for deriving elimination rules
    1.25 +  hypsubst.ML           tactic to substitute in the hypotheses
    1.26 +  ind.ML                a simple induction package
    1.27 +  quantifier1.ML	simplification procedures for "1 point rules"
    1.28 +  simp.ML               powerful but slow simplifier
    1.29 +  simplifier.ML         fast simplifier
    1.30 +  splitter.ML           performs case splits for simplifier.ML
    1.31 +  typedsimp.ML          basic simplifier for explicitly typed logics
    1.32  
    1.33  directory Arith:
    1.34 -  nat_transitive.ML     -- simple package for inequalities over nat
    1.35 -
    1.36 -
    1.37 -$Id$
    1.38 +  cancel_factor.ML	cancel common constant factor
    1.39 +  cancel_sums.ML	cancel common summands
    1.40 +  nat_transitive.ML	simple package for inequalities over nat