HOL-Algebra partially ported to Isar.
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
trans.ML transitivity reasoner for linear (total) orders
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