src/Provers/README
changeset 4289 5c1bfefd39b7
parent 3279 815ef5848324
child 4623 e6ada440a383
     1.1 --- a/src/Provers/README	Wed Nov 26 16:38:04 1997 +0100
     1.2 +++ b/src/Provers/README	Wed Nov 26 16:41:25 1997 +0100
     1.3 @@ -1,17 +1,23 @@
     1.4 -			Provers
     1.5 +
     1.6 +                        Provers
     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 -nat_transitive.ML -- simple package for inequalities over nat
    1.19 -simp.ML           -- powerful but slow simplifier
    1.20 -simplifier.ML     -- fast simplifier
    1.21 -splitter.ML       -- performs case splits for simplifier.ML
    1.22 -typedsimp.ML      -- basic simplifier for explicitly typed logics
    1.23 +blast.ML                -- generic tableau prover with proof reconstruction
    1.24 +classical.ML            -- theorem prover for classical logics
    1.25 +genelim.ML              -- bits and pieces for deriving elimination rules
    1.26 +hypsubst.ML             -- tactic to substitute in the hypotheses
    1.27 +ind.ML                  -- a simple induction package
    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$