src/Provers/README
changeset 3279 815ef5848324
parent 195 1315ce07f515
child 4289 5c1bfefd39b7
equal deleted inserted replaced
3278:636322bfd057 3279:815ef5848324
     1 			Provers
     1 			Provers
     2 
     2 
     3 This directory contains ML sources of generic theorem proving tools.
     3 This directory contains ML sources of generic theorem proving tools.
     4 Typically, they can be applied to various logics, provided rules of a
     4 Typically, they can be applied to various logics, provided rules of a
     5 certain form are derivable.  The first three are documented in the
     5 certain form are derivable.  Some of these are documented in the
     6 Reference Manual.
     6 Reference Manual.
     7 
     7 
     8 classical.ML  -- theorem prover for classical logics
     8 blast.ML          -- generic tableau prover with proof reconstruction
     9 hypsubst.ML   -- tactic to substitute in the hypotheses
     9 classical.ML      -- theorem prover for classical logics
    10 simplifier.ML -- fast simplifier
    10 genelim.ML        -- bits and pieces for deriving elimination rules
    11 simp.ML       -- powerful but slow simplifier
    11 hypsubst.ML       -- tactic to substitute in the hypotheses
    12 typedsimp.ML  -- basic simplifier for explicitly typed logics
    12 ind.ML            -- a simple induction package
    13 splitter.ML   -- performs case splits for simplifier.ML
    13 nat_transitive.ML -- simple package for inequalities over nat
    14 genelim.ML    -- bits and pieces for deriving elimination rules
    14 simp.ML           -- powerful but slow simplifier
    15 ind.ML        -- a simple induction package
    15 simplifier.ML     -- fast simplifier
       
    16 splitter.ML       -- performs case splits for simplifier.ML
       
    17 typedsimp.ML      -- basic simplifier for explicitly typed logics