--- a/Journal/document/root.tex	Tue Dec 19 14:20:29 2017 +0000
+++ b/Journal/document/root.tex	Wed Jan 10 00:28:17 2018 +0000
@@ -52,13 +52,14 @@
 \begin{document}
 \renewcommand{\thefootnote}{$\star$}
 \footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
-Compared with that paper we give an actual implementation of our formalised scheduling 
-algorithm in C and the operating system PINTOS. Our implementation follows closely all results
-we proved about optimisations of the Priority Inheritance Protocol.
 In Section 4 we improve our previous result by proving a finite bound for Priority Inversion.
 Moreover, we are giving in this paper
-more details about our proof and also surveying 
-the existing literature in more depth.}
+more details about our proof and describe some of our (unverified) C-code for implementing the
+Priority Inversion
+Protocol, as well as surveying 
+the existing literature in more depth.
+Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol.
+}
 \renewcommand{\thefootnote}{\arabic{footnote}}
 
 \title{Priority Inheritance Protocol Proved Correct$^\star$}
@@ -84,7 +85,7 @@
   overlap. Our formalisation in Isabelle/HOL is based on Paulson's
   inductive approach to verifying protocols.  The formalisation not
   only uncovers facts overlooked in the literature, but also helps
-  with an efficient implementation of this protocol. Earlier correct
+  with an efficient implementation of this protocol. Earlier
   implementations were criticised as too inefficient. Our
   implementation builds on top of the small PINTOS operating system
   used for teaching.\medskip