\doc{Changes required in old proof scripts}
\ref{changes}

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

\begin{itemize}
\item
Case is significant now in identifiers (but not in names).
\begin{verbatim}
Old: declare sort Nat               New: declare sort Nat
     declare operator 0: -> nat          declare operator 0: -> Nat
\end{verbatim}
\item
There are new symbols for the boolean operators.
\begin{verbatim}
Old: not, &, |                      New: ~, /\, \/
\end{verbatim}
(Fewer parentheses are needed now because the boolean operators \f{/\} and
\f{\/} bind more tightly than \f{=>}, which binds more tightly than \f{<=>}.)
\p
\item
There is now a single equality operator; i.e., ``double equals'' is gone.
\begin{verbatim}
Old: x + 0 == x                     New: x + 0 = x
     init(x) == x = 0                    init(x) <=> x = 0
     init(x) == x = 0                    init(x) = (x = 0)       
\end{verbatim}
\item
Declarations for infix operators need to be decorated with markers.  (Now users
can also declare prefix and postfix operators.)
\begin{verbatim}
Old: declare op +: N, N -> N        New: declare op __+__: N, N -> N
\end{verbatim}
\item
Assertions must be separated by semicolons. (Now users can mix arbitrary
assertions in the same \fq{assert} command.)
\begin{verbatim}
Old: assert ac +                    New: assert 
     assert                                ac +; 
       1 = s(0)                            1 = s(0); 
       x + 0 = x                           x + 0 = x
       ..                                  ..
\end{verbatim}
\item
Induction rules and partitioned-by's must begin with the keyword \fq{sort}.
\begin{verbatim}
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
\end{verbatim}
\item
Some qualifications added to disambiguate terms must be rewritten.
\begin{verbatim}
Old: assert a.b:S = 2               New: assert a.(b:S) = 2
     assert a:S[n]                       assert (a:S)[n]
\end{verbatim}
\item
Cases must be separated by commas.
\begin{verbatim}
Old: resume by case a b not(a | b)  New: resume by case a, b, ~(a \/ b)
\end{verbatim}
\item
Deduction rule hypotheses and conclusions must be separated by commas.
\begin{verbatim}
Old: when h1 h2 yield c1 c2         New: when h1, h2 yield c1, c2
\end{verbatim}
\item
Deduction rules now use the new notation for universal quantifiers.
\begin{verbatim}
Old: when forall x p(x) q(x)        New: when \A x p(x), \A x q(x) yield c
          yield c    
\end{verbatim}
\item
Commas and/or slashes are used now in name lists for the operations of union
and intersection.
\begin{verbatim}
Old: display d-r nat set            New: display d-r / (nat, set)
\end{verbatim}
\item
The annotations for box checking have been changed.  (It is best to let LP
regenerate them in a script file.)
\begin{verbatim}
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
\end{verbatim}
\end{itemize}

Users may have to make additional changes in their scripts because LP reacts
differently to them in the following ways.
\begin{itemize}
\item
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.
\item 
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.
\item
LP may generate different variable identifiers, e.g.,  when translating 
\fq{partitioned by}.
\item
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.
\end{itemize}