src/Provers/README
author wenzelm
Wed, 15 Oct 1997 15:12:59 +0200
changeset 3872 a5839ecee7b8
parent 3279 815ef5848324
child 4289 5c1bfefd39b7
permissions -rw-r--r--
tuned; prepare ext;

			Provers

This directory contains ML sources of generic theorem proving tools.
Typically, they can be applied to various logics, provided rules of a
certain form are derivable.  Some of these are documented in the
Reference Manual.

blast.ML          -- generic tableau prover with proof reconstruction
classical.ML      -- theorem prover for classical logics
genelim.ML        -- bits and pieces for deriving elimination rules
hypsubst.ML       -- tactic to substitute in the hypotheses
ind.ML            -- a simple induction package
nat_transitive.ML -- simple package for inequalities over nat
simp.ML           -- powerful but slow simplifier
simplifier.ML     -- fast simplifier
splitter.ML       -- performs case splits for simplifier.ML
typedsimp.ML      -- basic simplifier for explicitly typed logics