diff --git a/spec/changelog.tex b/spec/changelog.tex index a058885e76b3e0ac9ee087d7bf12470b9a681e55..0e0dc1b913653c8f2bd53f66a973f7d814abe3d5 100644 --- a/spec/changelog.tex +++ b/spec/changelog.tex @@ -1,3 +1,10 @@ +\subsection*{Unreleased} + +Braking changes: +\begin{itemize} + \item Allow arbitrary extra annotations in \texttt{assume} commands. +\end{itemize} + \subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}} This release overhauls the entire document, but introduces only few diff --git a/spec/doc.tex b/spec/doc.tex index cea62c5851bdf9ee04381167ff50d580484a131c..2ce54c6d3005efcca90755c57c20ae17dca8b2cb 100644 --- a/spec/doc.tex +++ b/spec/doc.tex @@ -691,7 +691,7 @@ An Alethe proof is a list of commands. \[ \begin{array}{r c l} \grNT{proof} &\grRule & \grNT{proof\_command}^{*} \\ - \grNT{proof\_command} &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\ + \grNT{proof\_command} &\grRule & \textAlethe{(assume}\; \grNT{symbol}\; \grNT{proof\_term}\;\grNT{attribute}^{*}\,\textAlethe{)} \\ &\grOr & \textAlethe{(step}\; \grNT{symbol}\; \grNT{clause} \; \textAlethe{:rule}\; \grNT{symbol} \\ & & \quad \grNT{premises\_annotation}^{?} \\