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

  hypsubst.ML           tactic to substitute in the hypotheses

  ind.ML                a simple induction package

  induct_method.ML      proof by cases and induction on sets and types (Isar)

  quantifier1.ML	simplification procedures for "1 point rules"

  simp.ML               powerful but slow simplifier

  simplifier.ML         fast simplifier

  split_paired_all.ML	turn surjective pairing into split rule

  splitter.ML           performs case splits for simplifier.ML

  typedsimp.ML          basic simplifier for explicitly typed logics

directory Arith:

  abel_cancel.ML	cancel complementary terms in sums of Abelian groups

  assoc_fold.ML		fold numerals in nested products

  cancel_numerals.ML	cancel common coefficients in balanced expressions

  cancel_factor.ML	cancel common constant factor

  cancel_sums.ML	cancel common summands

  combine_numerals.ML	combine coefficients in expressions

  fast_lin_arith.ML	generic linear arithmetic package