LP, the Larch Prover  New features in Release 3.1
The following features have been added to LP since Release 2.4.

Support for full firstorder logic, not just the universalexistential subset
supported by Release 2.4. See quantifiers.

A simple sort system for describing polymorphic abstractions.

New inference mechanisms

Proofs by well founded induction.

Proofs of conjectures of the form t1 <=> t2, with t1 => t2
and t2 => t1 as subgoals.

Proofs that use deduction rules for backward inference. See apply.

Richer syntactic conventions, such as x[n] and n!, for
operators and terms.

Additional user amenities, for example, enhanced facilities for
naming sets of statements.

New rewrite rule for the boolean operators, namely, ~p <=> ~q > p <=> q.
The following features behave differently in Release 3.1 than they did in
Release 2.4.

Some settings (e.g., the default name prefix) are
now local to proof contexts.

Names such as thmCaseHyp1.1 are reused within nonoverlapping proof
contexts.

LP now attempts to preserve the order of operands in formulas such as
init => c = 1, so that preference is given to ordering equalities in the
direction the user may have intended when these formulas normalize to
equations.