diff --git a/docs/bib.bib b/docs/bib.bib
index db38003884989ad60c86be1638b61ed6018a5ea4..a8f88cf36dc4d36cecc3593fcfc196b49c4156af 100644
--- a/docs/bib.bib
+++ b/docs/bib.bib
@@ -3836,3 +3836,16 @@ year = {2013}
 	journal={Submitted to JFP},
         year  = {2017},
 }
+
+@article{Loeb,
+ ISSN = {00224812},
+ URL = {http://www.jstor.org/stable/2266895},
+ author = {Martin H. Löb},
+ journal = {The Journal of Symbolic Logic},
+ number = {2},
+ pages = {115--118},
+ publisher = {Association for Symbolic Logic},
+ title = {Solution of a Problem of Leon Henkin},
+ volume = {20},
+ year = {1955}
+}
diff --git a/docs/ghost-state.tex b/docs/extended-logic.tex
similarity index 99%
rename from docs/ghost-state.tex
rename to docs/extended-logic.tex
index 7dbf916a9f9d0f1e8b8b9558acedcc1edb5e8d89..b668805abca0474014aa44d2b5b39e4817883d7f 100644
--- a/docs/ghost-state.tex
+++ b/docs/extended-logic.tex
@@ -41,8 +41,8 @@ We collect here some important and frequently used derived proof rules.
   {\TRUE \proves \plainly\TRUE}
 \end{mathparpagebreakable}
 
-Noteworthy here is the fact that Löb induction can be derived from $\later$-introduction and the fact that we can take fixed-points of functions where the recursive occurrences are below $\later$.%
-\footnote{See \url{https://en.wikipedia.org/wiki/L\%C3\%B6b\%27s_theorem}.}
+Noteworthy here is the fact that Löb induction can be derived from $\later$-introduction and the fact that we can take fixed-points of functions where the recursive occurrences are below $\later$~\cite{Loeb}.%
+\footnote{Also see \url{https://en.wikipedia.org/wiki/L\%C3\%B6b\%27s_theorem}.}
 Furthermore, $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.
 To derive that existential quantifiers commute with separating conjunction requires an intermediate step using a magic wand: From $P * \exists x, Q \vdash \Exists x. P * Q$ we can deduce $\Exists x. Q \vdash P \wand \Exists x. P * Q$ and then proceed via $\exists$-elimination.
 
diff --git a/docs/iris.tex b/docs/iris.tex
index 4c74119f53f99e9c967b761a3d0379561376f77f..d4c5dc8a4e9da0e7a24a25a0c6f180e47add2770 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -56,7 +56,7 @@ For a list of changes in Iris since then, please consult our changelog at \url{h
 \input{model}
 \endgroup
 \clearpage\begingroup
-\input{ghost-state}
+\input{extended-logic}
 \endgroup
 \clearpage\begingroup
 \input{language}