author  wenzelm 
Fri, 19 Oct 2001 22:02:25 +0200  
changeset 11840  54fe56353704 
parent 8870  e900a58cafe4 
child 13735  7de9342aca7a 
permissions  rwrr 
4623  1 
Provers: generic theorem proving tools 
0  2 

3 
This directory contains ML sources of generic theorem proving tools. 

4 
Typically, they can be applied to various logics, provided rules of a 

3279  5 
certain form are derivable. Some of these are documented in the 
195  6 
Reference Manual. 
0  7 

4623  8 
blast.ML generic tableau prover with proof reconstruction 
4654  9 
clasimp.ML combination of classical reasoner and simplifier 
4623  10 
classical.ML theorem prover for classical logics 
11 
hypsubst.ML tactic to substitute in the hypotheses 

12 
ind.ML a simple induction package 

11840
54fe56353704
induct_method.ML  proof by cases and induction on sets and types (Isar);
wenzelm
parents:
8870
diff
changeset

13 
induct_method.ML proof by cases and induction on sets and types (Isar) 
4623  14 
quantifier1.ML simplification procedures for "1 point rules" 
15 
simp.ML powerful but slow simplifier 

16 
simplifier.ML fast simplifier 

5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
4654
diff
changeset

17 
split_paired_all.ML turn surjective pairing into split rule 
4623  18 
splitter.ML performs case splits for simplifier.ML 
19 
typedsimp.ML basic simplifier for explicitly typed logics 

4289  20 

21 
directory Arith: 

8870  22 
abel_cancel.ML cancel complementary terms in sums of Abelian groups 
23 
assoc_fold.ML fold numerals in nested products 

24 
cancel_numerals.ML cancel common coefficients in balanced expressions 

4623  25 
cancel_factor.ML cancel common constant factor 
26 
cancel_sums.ML cancel common summands 

8870  27 
combine_numerals.ML combine coefficients in expressions 
28 
fast_lin_arith.ML generic linear arithmetic package 