From 9fc80517358aab7721120f6293e3cb8e48272d82 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Jun 2019 10:50:25 +0200
Subject: [PATCH] =?UTF-8?q?rename=20'extensions'=20section=20file;=20add?=
 =?UTF-8?q?=20reference=20to=20L=C3=B6b's=20paper?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 docs/bib.bib                                 | 13 +++++++++++++
 docs/{ghost-state.tex => extended-logic.tex} |  4 ++--
 docs/iris.tex                                |  2 +-
 3 files changed, 16 insertions(+), 3 deletions(-)
 rename docs/{ghost-state.tex => extended-logic.tex} (99%)

diff --git a/docs/bib.bib b/docs/bib.bib
index db3800388..a8f88cf36 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 7dbf916a9..b668805ab 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 4c74119f5..d4c5dc8a4 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}
-- 
GitLab