src/Provers/README
author wenzelm
Wed Nov 26 16:41:25 1997 +0100 (1997-11-26)
changeset 4289 5c1bfefd39b7
parent 3279 815ef5848324
child 4623 e6ada440a383
permissions -rw-r--r--
tuned;
     1 
     2                         Provers
     3 
     4 This directory contains ML sources of generic theorem proving tools.
     5 Typically, they can be applied to various logics, provided rules of a
     6 certain form are derivable.  Some of these are documented in the
     7 Reference Manual.
     8 
     9 blast.ML                -- generic tableau prover with proof reconstruction
    10 classical.ML            -- theorem prover for classical logics
    11 genelim.ML              -- bits and pieces for deriving elimination rules
    12 hypsubst.ML             -- tactic to substitute in the hypotheses
    13 ind.ML                  -- a simple induction package
    14 simp.ML                 -- powerful but slow simplifier
    15 simplifier.ML           -- fast simplifier
    16 splitter.ML             -- performs case splits for simplifier.ML
    17 typedsimp.ML            -- basic simplifier for explicitly typed logics
    18 
    19 directory Arith:
    20   nat_transitive.ML     -- simple package for inequalities over nat
    21 
    22 
    23 $Id$