Add 0.3 description to changelog

spec/changelog.tex

+\subsection*{0.3 --- Unreleased}
+
+This release overhauls the entire document, but introduces only few
+changes to the proof format itself.
+
+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.
+\begin{itemize}
+	\item An abstract proof checking procedure to clarify
+	the semantic of the proof format was added.
+	\item A description of the semantic 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.,
+   $(f\;x\;(g\;y))$).  This only a change in notation -- the used logic
+   remains many-sorted first-order logic.
+  \item The is no longer a distinction between if-and-only-if and
+   equaltiy.  Instead equality (the symbol $≈$) is used with appropiate
+   sorts.
+  \item An index that lists all proof rules was added.
+\end{itemize}
+
 \subsection*{0.2 --- \DTMdisplaydate{2022}{12}{19}{-1}}
 
 This is an intermediate release.  It collects all changes to the original