diff --git a/docs/bib.bib b/docs/bib.bib
index 239c73fc4372409f6f18d9ec1aad2e0af4fec1d9..db38003884989ad60c86be1638b61ed6018a5ea4 100644
--- a/docs/bib.bib
+++ b/docs/bib.bib
@@ -3829,3 +3829,10 @@ year = {2013}
   pages     = {256--269},
   year      = {2016},
 }
+
+@Article{iris-ground-up,
+	author={Ralf Jung and Robbert Krebbers and Jacques-Henri Jourdan and Ale\v{s} Bizjak and Lars Birkedal and Derek Dreyer},
+	title={Iris from the Ground Up},
+	journal={Submitted to JFP},
+        year  = {2017},
+}
diff --git a/docs/iris.tex b/docs/iris.tex
index dfe6a1dbc75fb3121ae453c90d5fc7b91579f9e3..d91eaac0b24f6a47903af775d8956393b4a99e5b 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -32,28 +32,49 @@ The latest versions of this document and the Coq formalization can be found in t
 For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
 \end{abstract}
 
-\clearpage
+\clearpage\begingroup
 \tableofcontents
+\endgroup
+
+\clearpage\begingroup
+\section{Revision History}
+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 \ralf{TODO: WP stuckness bits.}
+\end{itemize}
+\endgroup
 
 \clearpage\begingroup
 \input{algebra}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \input{constructions}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \input{base-logic}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \input{model}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \input{ghost-state}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \input{language}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \input{program-logic}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \input{derived}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \input{paradoxes}
-\endgroup\clearpage\begingroup
+\endgroup
+\clearpage\begingroup
 \printbibliography
 \endgroup