refer to journal paper

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},
+}

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