diff --git a/CHANGELOG.md b/CHANGELOG.md
index 18b28cab9545f72bab80d5c098096a27a09bc3da..9a6df74fba6060b839082cb6790f22eef3a20e42 100644
--- a/CHANGELOG.md
+++ b/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
diff --git a/docs/iris.tex b/docs/iris.tex
index bd5792b41d29d3b9f9cc9b3ddfec1f2bcd7e074f..c227a50d6bc886d3982fee1340587dc5410c786d 100644
--- a/docs/iris.tex
+++ b/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