author  wenzelm 
Sun, 22 May 2005 16:51:07 +0200  
changeset 16019  0e1405402d53 
parent 13736  6ea0e7c43c4f 
child 30159  7b55b6b5c0c2 
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) 
13736
6ea0e7c43c4f
Transitivity reasoner renamed to linorder.ML. README updated.
ballarin
parents:
13735
diff
changeset

14 
linorder.ML transitivity reasoner for linear (total) orders 
4623  15 
quantifier1.ML simplification procedures for "1 point rules" 
16 
simp.ML powerful but slow 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 
16019  18 
splitter.ML performs case splits for simplifier 
4623  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 