LP, the Larch Prover — Changes from Release 2.4 to Release 3.1

Users must observe the following new syntactic conventions when using Release 3.1 instead of Release 2.4.

Case is significant now in identifiers (but not in names).

Old: declare sort Nat               New: declare sort Nat
     declare operator 0: -> nat          declare operator 0: -> Nat

There are new symbols for the boolean operators.
```
Old: not, &, |                      New: ~, /\, \/
```
(Fewer parentheses are needed now because the boolean operators /\ and \/ bind more tightly than =>, which binds more tightly than <=>.)

There is now a single equality operator; i.e., ``double equals'' is gone.

Old: x + 0 == x                     New: x + 0 = x
     init(x) == x = 0                    init(x) <=> x = 0
     init(x) == x = 0                    init(x) = (x = 0)

Declarations for infix operators need to be decorated with markers. (Now users can also declare prefix and postfix operators.)
```
Old: declare op +: N, N -> N        New: declare op __+__: N, N -> N
```

Assertions must be separated by semicolons. (Now users can mix arbitrary assertions in the same assert command.)

Old: assert ac +                    New: assert 
     assert                                ac +; 
       1 = s(0)                            1 = s(0); 
       x + 0 = x                           x + 0 = x
       ..                                  ..

Induction rules and partitioned-by's must begin with the keyword sort.

Old: assert Nat generated by 0, s   New: assert sort Nat generated by 0, s
     assert Set parititioned by /in      assert sort Set partitioned by \in

Some qualifications added to disambiguate terms must be rewritten.

Old: assert a.b:S = 2               New: assert a.(b:S) = 2
     assert a:S[n]                       assert (a:S)[n]

Cases must be separated by commas.

Old: resume by case a b not(a | b)  New: resume by case a, b, ~(a \/ b)

Deduction rule hypotheses and conclusions must be separated by commas.
```
Old: when h1 h2 yield c1 c2         New: when h1, h2 yield c1, c2
```

Deduction rules now use the new notation for universal quantifiers.

Old: when forall x p(x) q(x)        New: when \A x p(x), \A x q(x) yield c
          yield c

Commas and/or slashes are used now in name lists for the operations of union and intersection.
```
Old: display d-r nat set            New: display d-r / (nat, set)
```

The annotations for box checking have been changed. (It is best to let LP regenerate them in a script file.)

Old: prove P(x) by case x = 0       New: prove P(x) by case x = 0
       <> 2 subgoals for proof              <> case xc = 0
         ... commands ...                   ... commands ...
         [] case 0 = xc                     [] case xc = 0
         ... commands ...                   <> case ~(xc = 0)
         [] case not(0 = xc)                ... commands ...
       [] conjecture                        [] case ~(xc = 0)
                                          [] conjecture

Users may have to make additional changes in their scripts because LP reacts differently to them in the following ways.

LP may orient some equations (e.g., case hypotheses) in the opposite direction. Many times, the new direction will be the one the user desired. But the new direction may cause LP to compute different critical pairs.
LP flattens terms differently, because new spellings for (the boolean) operators collate differently. This may result in different reduction sequences during normalization, which may cause some proofs to succeed faster, some to succeed slower, and some to fail entirely.
LP may generate different variable identifiers, e.g., when translating partitioned by.
LP formulates the proof obligation for a deduction rule as an implication. This enables users to prove deduction rules using induction. However, box-checking now supplies/requires different annotations.