diff --git a/spec/changelog.tex b/spec/changelog.tex index ca49bf19df551dd9f09522b1e8624e0d3acda11c..7abf17856232ab94f5471dc4159551c6e98a96d3 100644 --- a/spec/changelog.tex +++ b/spec/changelog.tex @@ -7,23 +7,21 @@ The standard now specifies that \texttt{assume} commands can only be issued at the start of the proof or right after an \texttt{anchor} command. -Beyond many smaller clarifications and typographic improvments, the -following changes were implemented in this release. +Beyond many smaller clarifications and typographic improvements, the +following changes are implemented in this release. \begin{itemize} - \item An abstract proof checking procedure to clarify - the semantics of the proof format was added. - \item A description of the semantics of contexts based on λ-terms - was added. - \item The document now lists all transformations that are - implicit in Alethe proofs. - \item The notation used for terms from first-order style - (e.g., $f(x,g(y))$) was changed to higher-order style (e.g., + \item Add an abstract proof checking procedure to clarify + the semantics of the proof format. + \item Add a description of the semantics of contexts based on λ-terms. + \item List all transformations that are implicit in Alethe proofs. + \item Change the notation used for terms from first-order style + (e.g., $f(x,g(y))$) to higher-order style (e.g., $(f\;x\;(g\;y))$). This is only a change in notation -- the used logic remains many-sorted first-order logic. - \item There is no longer a distinction between if-and-only-if and - equaltiy. Instead equality (the symbol $≈$) is used with appropiate + \item Eliminate the distinction between if-and-only-if and + equality. Instead, use equality (the symbol $≈$) with appropriate sorts. - \item An index that lists all proof rules was added. + \item Add an index that lists all proof rules. \end{itemize} Proof rules: