--- a/Journal/document/root.tex	Wed Dec 19 12:51:06 2012 +0000
+++ b/Journal/document/root.tex	Wed Dec 19 23:46:36 2012 +0000
@@ -68,12 +68,14 @@
 the Property Inheritance Protocol presents a correctness ``proof'' for
 an \emph{incorrect} algorithm. In this paper we fix the problem of
 this proof by making all notions precise and implementing a variant of
-a solution proposed earlier. Our formalisation in Isabelle/HOL
+a solution proposed earlier. We also generalise the result 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
 were criticised as too inefficient. Our formalisation is based on
 Paulson's inductive approach to verifying protocols; our implementation
-is on top of the small PINTOS operating system.\medskip
+builds on top of the small PINTOS operating system.\medskip
 
 %{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
 %real-time systems, Isabelle/HOL