summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Provers/README

changeset 0 | a5a9c433f639 |

child 195 | 1315ce07f515 |

--- /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