src/Provers/README

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/README	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,12 @@
+			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