1 
1 Provers: generic theorem proving tools 
2 Provers 

3 
2 
4 This directory contains ML sources of generic theorem proving tools. 
3 This directory contains ML sources of generic theorem proving tools. 
5 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 
6 certain form are derivable. Some of these are documented in the 
5 certain form are derivable. Some of these are documented in the 
7 Reference Manual. 
6 Reference Manual. 
8 
7 
9 blast.ML  generic tableau prover with proof reconstruction 
8 blast.ML generic tableau prover with proof reconstruction 
10 classical.ML  theorem prover for classical logics 
9 classical.ML theorem prover for classical logics 
11 genelim.ML  bits and pieces for deriving elimination rules 
10 genelim.ML bits and pieces for deriving elimination rules 
12 hypsubst.ML  tactic to substitute in the hypotheses 
11 hypsubst.ML tactic to substitute in the hypotheses 
13 ind.ML  a simple induction package 
12 ind.ML a simple induction package 
14 simp.ML  powerful but slow simplifier 
13 quantifier1.ML simplification procedures for "1 point rules" 
15 simplifier.ML  fast simplifier 
14 simp.ML powerful but slow simplifier 
16 splitter.ML  performs case splits for simplifier.ML 
15 simplifier.ML fast simplifier 
17 typedsimp.ML  basic simplifier for explicitly typed logics 
16 splitter.ML performs case splits for simplifier.ML 

17 typedsimp.ML basic simplifier for explicitly typed logics 
18 
18 
19 directory Arith: 
19 directory Arith: 
20 nat_transitive.ML  simple package for inequalities over nat 
20 cancel_factor.ML cancel common constant factor 
21 
21 cancel_sums.ML cancel common summands 
22 
22 nat_transitive.ML simple package for inequalities over nat 
23 $Id$ 
