src/Provers/README
author lcp
Mon Dec 13 18:48:47 1993 +0100 (1993-12-13)
changeset 195 1315ce07f515
parent 0 a5a9c433f639
child 3279 815ef5848324
permissions -rw-r--r--
added mention of simplifier, splitter, hypsubst
clasohm@0
     1
			Provers
clasohm@0
     2
clasohm@0
     3
This directory contains ML sources of generic theorem proving tools.
clasohm@0
     4
Typically, they can be applied to various logics, provided rules of a
lcp@195
     5
certain form are derivable.  The first three are documented in the
lcp@195
     6
Reference Manual.
clasohm@0
     7
lcp@195
     8
classical.ML  -- theorem prover for classical logics
lcp@195
     9
hypsubst.ML   -- tactic to substitute in the hypotheses
lcp@195
    10
simplifier.ML -- fast simplifier
lcp@195
    11
simp.ML       -- powerful but slow simplifier
lcp@195
    12
typedsimp.ML  -- basic simplifier for explicitly typed logics
lcp@195
    13
splitter.ML   -- performs case splits for simplifier.ML
lcp@195
    14
genelim.ML    -- bits and pieces for deriving elimination rules
lcp@195
    15
ind.ML        -- a simple induction package