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

src/Provers/README

author | clasohm |

Thu, 16 Sep 1993 12:20:38 +0200 | |

changeset 0 | a5a9c433f639 |

child 195 | 1315ce07f515 |

permissions | -rw-r--r-- |

Initial revision

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