src/Provers/README
author nipkow
Fri, 09 Oct 1998 14:19:13 +0200
changeset 5633 fb7fa1b154c4
parent 4654 dbeae12ada20
child 5680 4f526bcd3a68
permissions -rw-r--r--
Added a few breaks in error text.

                 Provers: generic theorem proving tools

This directory contains ML sources of generic theorem proving tools.
Typically, they can be applied to various logics, provided rules of a
certain form are derivable.  Some of these are documented in the
Reference Manual.

  blast.ML              generic tableau prover with proof reconstruction
  clasimp.ML		combination of classical reasoner and simplifier
  classical.ML          theorem prover for classical logics
  genelim.ML            bits and pieces for deriving elimination rules
  hypsubst.ML           tactic to substitute in the hypotheses
  ind.ML                a simple induction package
  quantifier1.ML	simplification procedures for "1 point rules"
  simp.ML               powerful but slow simplifier
  simplifier.ML         fast simplifier
  splitter.ML           performs case splits for simplifier.ML
  typedsimp.ML          basic simplifier for explicitly typed logics

directory Arith:
  cancel_factor.ML	cancel common constant factor
  cancel_sums.ML	cancel common summands
  nat_transitive.ML	simple package for inequalities over nat