--- a/Journal/Paper.thy	Tue Dec 19 14:20:29 2017 +0000
+++ b/Journal/Paper.thy	Wed Jan 10 00:28:17 2018 +0000
@@ -138,10 +138,9 @@
   implementations and PIP being too complicated and too inefficient.
   For example, Yodaiken writes in \cite{Yodaiken02}:
 
-  \begin{quote}
-  \it{}``Priority inheritance is neither efficient nor reliable. Implementations
-  are either incomplete (and unreliable) or surprisingly complex and intrusive.''
-  \end{quote}
+  \begin{quote} \it{}``Priority inheritance is neither efficient nor
+  reliable. Implementations are either incomplete (and unreliable) or
+  surprisingly complex and intrusive.''  \end{quote}
 
   \noindent He suggests avoiding PIP altogether by designing the
   system so that no priority inversion may happen in the first
@@ -2137,10 +2136,12 @@
   be recalculated for an event. This information is provided by the lemmas we proved.
   We confirmed that our observations translate into practice by implementing
   our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at 
-  Stanford University \cite{PINTOS}. An alternative would have been the small Xv6 operating 
+  Stanford University \cite{PINTOS}.\footnote{An alternative would have been the small Xv6 operating 
   system used for teaching at MIT \cite{Xv6link,Xv6}. However this operating system implements
   a simple round robin scheduler that lacks stubs for dealing with priorities. This
-  is inconvenient for our purposes.
+  is inconvenient for our purposes.} While there is no formal connection between our
+  formalisation and the C-code shown below, the results of the formalisation clearly 
+  shine through in the design of the code.
 
 
   To implement PIP in PINTOS, we only need to modify the kernel