docs: for now we won't document atomic triples or total triples;...

docs: for now we won't document atomic triples or total triples; de-experimentalize plainly and stuckness

CHANGELOG.md

@@ -14,9 +14,9 @@ Changes in and extensions of the theory:
 * [#] Weaken the semantics of CAS in heap_lang to be efficiently implementable:
   CAS may only be used to compare "unboxed" values that can be represented in a
   single machine word.
-* [#] Add weakest preconditions for total program correctness.
-* [#] "(Potentially) stuck" weakest preconditions are no longer considered
-  experimental.
+* Add weakest preconditions for total program correctness.
+* "(Potentially) stuck" weakest preconditions and the "plainly modality" are no
+  longer considered experimental.
 * The adequacy statement for weakest preconditions now also involves the
   final state.
 * [#] Add the notion of an "observation" to the language interface, so that

docs/iris.tex

@@ -40,11 +40,7 @@ For further information, visit the Iris project website at \url{http://plv.mpi-s
 \section{Iris from the Ground Up}
 In \citetitle{iris-ground-up}~\cite{iris-ground-up}, we describe Iris~3.1 in a bottom-up way.
 That paper is hence much more suited as an introduction to the model of Iris than this reference, which mostly contains definitions, not explanations or examples.
-The following differences between Iris as described in \citetitle{iris-ground-up} and the latest version documented here are worth mentioning:
-\begin{itemize}
-\item As an experimental feature, we added the \emph{plainly modality} $\plainly$.
-\item As an experimental feature, weakest preconditions take a \emph{stuckness} $\stuckness$ as parameter, indicating whether the program may get stuck or not.
-\end{itemize}
+For a list of changes in Iris since then, please consult \href{https://gitlab.mpi-sws.org/iris/iris/blob/master/CHANGELOG.md}{our changelog}.
 \endgroup
 
 \clearpage\begingroup