From 64c34e7e393c6e9e64f7c723e76278a20a95d41c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 22 Oct 2016 13:49:50 +0200
Subject: [PATCH] docs: add a small abstract with more links

---
 docs/iris.tex | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/docs/iris.tex b/docs/iris.tex
index ca5b8ff16..4813b2701 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -15,15 +15,24 @@
 
 \input{setup}
 
-\begin{document}
 
 \title{\bfseries The Iris 2.0 Documentation}
 \author{\url{http://plv.mpi-sws.org/iris/}}
-\maketitle
 
-\thispagestyle{empty}
 
-%\clearpage
+\begin{document}
+
+\maketitle
+\thispagestyle{empty}
+\vfill
+\begin{abstract}
+This document describes formally the Iris program logic.
+Every result in this document has been fully verified in Coq.
+The latest versions of this document and the Coq formalization can be found in the git repository at \url{https://gitlab.mpi-sws.org/FP/iris-coq/}.
+For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
+\end{abstract}
+
+\clearpage
 \tableofcontents
 
 \clearpage\begingroup
-- 
GitLab