From 785e0a3d0fdc271e1a419b0c1d33a2a6982b3a80 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Fri, 23 Dec 2022 11:55:32 +0100
Subject: [PATCH] Add 0.3 description to changelog

---
 spec/changelog.tex | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/spec/changelog.tex b/spec/changelog.tex
index 77fdee6..0589563 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -1,3 +1,31 @@
+\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
-- 
GitLab