LP, the Larch Prover -- Release 3.1b

The following bugs in Version 3.1a have been fixed in Version 3.1b.
The normalize command now properly normalizes a rewrite rule with a reducible left side.
The operation of boolean equality is now recognized as an ac operator, and not just as a commutative operator.
The experimental version of LP (invoked by lp -e) no longer crashes when a register command is issued during a proof.
The bound variable i1 in
 f(i, j) <=> \A i1 \A j1 (i ~= i1 \/ j ~= j1 => P(i1, j1))
is no longer changed incorrectly to i2 when executing show normal-form f(i2, i1).
In addition, the following improvements have been made in Version 3.1b.