--- a/Journal/document/root.tex	Wed Mar 12 10:08:20 2014 +0000
+++ b/Journal/document/root.tex	Tue May 06 14:36:40 2014 +0100
@@ -18,6 +18,7 @@
 \usepackage{url}
 \usepackage{color}
 \usepackage{courier}
+\usetikzlibrary{patterns}
 \usepackage{listings}
 \lstset{language=C,
         numbers=left,
@@ -49,7 +50,10 @@
 
 \begin{document}
 \renewcommand{\thefootnote}{$\star$}
-\footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.}
+\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.}
 \renewcommand{\thefootnote}{\arabic{footnote}}
 
 \title{Priority Inheritance Protocol Proved Correct}
@@ -73,11 +77,11 @@
 a solution proposed earlier. We also generalise the original informal proof to the
 practically relevant case where critical sections can
 overlap. Our formalisation in Isabelle/HOL not just
-uncovers facts not mentioned in the literature, but also shows how to
-efficiently implement this protocol. Earlier correct implementations
+uncovers facts not mentioned in the literature, but also helps with
+implementing efficiently this protocol. Earlier correct implementations
 were criticised as too inefficient. Our formalisation is based on
 Paulson's inductive approach to verifying protocols; our implementation
-builds on top of the small PINTOS operating system.\medskip
+builds on top of the small PINTOS operating system used for teaching.\medskip
 
 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
 %real-time systems, Isabelle/HOL