author  wenzelm 
Mon, 16 Nov 1998 13:54:35 +0100  
changeset 5897  b3548f939dd2 
parent 5680  4f526bcd3a68 
child 8870  e900a58cafe4 
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 

13 
quantifier1.ML simplification procedures for "1 point rules" 

14 
simp.ML powerful but slow simplifier 

15 
simplifier.ML fast simplifier 

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

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

4289  19 

20 
directory Arith: 

4623  21 
cancel_factor.ML cancel common constant factor 
22 
cancel_sums.ML cancel common summands 

23 
nat_transitive.ML simple package for inequalities over nat 