src/Provers/README

logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
So it no longer checks t properly -- but it never checked u anyway, and all
existing calls are derived from certified terms...

			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.  Unfortunately, little documentation is
available.

classical.ML -- theorem prover for classical logics
genelim.ML   -- bits and pieces for deriving elimination rules
ind.ML       -- a simple induction package
simp.ML      -- a powerful simplifier
typedsimp.ML -- a rather basic simplifier for explicitly typed logics