equal
deleted
inserted
replaced
4 Typically, they can be applied to various logics, provided rules of a |
4 Typically, they can be applied to various logics, provided rules of a |
5 certain form are derivable. Some of these are documented in the |
5 certain form are derivable. Some of these are documented in the |
6 Reference Manual. |
6 Reference Manual. |
7 |
7 |
8 blast.ML generic tableau prover with proof reconstruction |
8 blast.ML generic tableau prover with proof reconstruction |
|
9 clasimp.ML combination of classical reasoner and simplifier |
9 classical.ML theorem prover for classical logics |
10 classical.ML theorem prover for classical logics |
10 genelim.ML bits and pieces for deriving elimination rules |
11 genelim.ML bits and pieces for deriving elimination rules |
11 hypsubst.ML tactic to substitute in the hypotheses |
12 hypsubst.ML tactic to substitute in the hypotheses |
12 ind.ML a simple induction package |
13 ind.ML a simple induction package |
13 quantifier1.ML simplification procedures for "1 point rules" |
14 quantifier1.ML simplification procedures for "1 point rules" |