src/Provers/README
author clasohm
Tue, 24 Oct 1995 14:45:35 +0100
changeset 1294 1358dc040edb
parent 195 1315ce07f515
child 3279 815ef5848324
permissions -rw-r--r--
added calls of init_html and make_chart; added usage of qed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
			Provers
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
This directory contains ML sources of generic theorem proving tools.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
Typically, they can be applied to various logics, provided rules of a
195
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
     5
certain form are derivable.  The first three are documented in the
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
     6
Reference Manual.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
195
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
     8
classical.ML  -- theorem prover for classical logics
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
     9
hypsubst.ML   -- tactic to substitute in the hypotheses
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
    10
simplifier.ML -- fast simplifier
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
    11
simp.ML       -- powerful but slow simplifier
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
    12
typedsimp.ML  -- basic simplifier for explicitly typed logics
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
    13
splitter.ML   -- performs case splits for simplifier.ML
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
    14
genelim.ML    -- bits and pieces for deriving elimination rules
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
    15
ind.ML        -- a simple induction package