author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 195 1315ce07f515
permissions -rw-r--r--
Initial revision


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

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