0 a5a9c433f639 Initial revision clasohm parents: diff changeset ` 1` ``` Provers ``` a5a9c433f639 Initial revision clasohm parents: diff changeset ` 2` a5a9c433f639 Initial revision clasohm parents: diff changeset ` 3` ```This directory contains ML sources of generic theorem proving tools. ``` a5a9c433f639 Initial revision clasohm parents: diff changeset ` 4` ```Typically, they can be applied to various logics, provided rules of a ``` 195 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 5` ```certain form are derivable. The first three are documented in the ``` 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 6` ```Reference Manual. ``` 0 a5a9c433f639 Initial revision clasohm parents: diff changeset ` 7` 195 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 8` ```classical.ML -- theorem prover for classical logics ``` 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 9` ```hypsubst.ML -- tactic to substitute in the hypotheses ``` 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 10` ```simplifier.ML -- fast simplifier ``` 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 11` ```simp.ML -- powerful but slow simplifier ``` 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 12` ```typedsimp.ML -- basic simplifier for explicitly typed logics ``` 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 13` ```splitter.ML -- performs case splits for simplifier.ML ``` 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 14` ```genelim.ML -- bits and pieces for deriving elimination rules ``` 1315ce07f515 added mention of simplifier, splitter, hypsubst lcp parents: 0 diff changeset ` 15` ```ind.ML -- a simple induction package ```