| author | clasohm |
| Thu, 16 Sep 1993 12:20:38 +0200 | |
| changeset 0 | a5a9c433f639 |
| child 195 | 1315ce07f515 |
| permissions | -rw-r--r-- |
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