author wenzelm Wed Apr 04 00:11:03 2007 +0200 (2007-04-04) changeset 22578 b0eb5652f210 parent 16019 0e1405402d53 child 30159 7b55b6b5c0c2 permissions -rw-r--r--
removed obsolete sign_of/sign_of_thm;
```     1                  Provers: generic theorem proving tools
```
```     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
```
```     5 certain form are derivable.  Some of these are documented in the
```
```     6 Reference Manual.
```
```     7
```
```     8   blast.ML              generic tableau prover with proof reconstruction
```
```     9   clasimp.ML		combination of classical reasoner and simplifier
```
```    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   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"
```
```    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
```
```    19   typedsimp.ML          basic simplifier for explicitly typed logics
```
```    20
```
```    21 directory Arith:
```
```    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
```
```    25   cancel_factor.ML	cancel common constant factor
```
```    26   cancel_sums.ML	cancel common summands
```
```    27   combine_numerals.ML	combine coefficients in expressions
```
```    28   fast_lin_arith.ML	generic linear arithmetic package
```