1 Provers: generic theorem proving tools 
1 Provers: generic theorem proving tools 
2 
2 
3 This directory contains ML sources of generic theorem proving tools. 
3 This directory contains ML sources of generic theorem proving tools. 
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. 
6 Reference Manual. 

7 
6 
8 blast.ML generic tableau prover with proof reconstruction 
7 blast.ML generic tableau prover with proof reconstruction 
9 clasimp.ML combination of classical reasoner and simplifier 
8 clasimp.ML combination of classical reasoner and simplifier 
10 classical.ML theorem prover for classical logics 
9 classical.ML theorem prover for classical logics 
11 hypsubst.ML tactic to substitute in the hypotheses 
10 hypsubst.ML tactic to substitute in the hypotheses 
12 ind.ML a simple induction package 

13 induct_method.ML proof by cases and induction on sets and types (Isar) 

14 linorder.ML transitivity reasoner for linear (total) orders 

15 quantifier1.ML simplification procedures for "1 point rules" 
11 quantifier1.ML simplification procedures for "1 point rules" 
16 simp.ML powerful but slow simplifier 

17 split_paired_all.ML turn surjective pairing into split rule 

18 splitter.ML performs case splits for simplifier 
12 splitter.ML performs case splits for simplifier 
19 typedsimp.ML basic simplifier for explicitly typed logics 
13 typedsimp.ML basic simplifier for explicitly typed logics 
20 
14 
21 directory Arith: 
15 directory Arith: 
22 abel_cancel.ML cancel complementary terms in sums of Abelian groups 
16 abel_cancel.ML cancel complementary terms in sums of Abelian groups 