0

1 
Provers


2 


3 
This directory contains ML sources of generic theorem proving tools.


4 
Typically, they can be applied to various logics, provided rules of a


5 
certain form are derivable. Unfortunately, little documentation is


6 
available.


7 


8 
classical.ML  theorem prover for classical logics


9 
genelim.ML  bits and pieces for deriving elimination rules


10 
ind.ML  a simple induction package


11 
simp.ML  a powerful simplifier


12 
typedsimp.ML  a rather basic simplifier for explicitly typed logics
