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


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.  The first three are documented in the
Reference Manual.

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