Fix typos in changelog

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: