diff -r 242a781135ba -r 8e02fb168350 Journal/document/root.tex --- a/Journal/document/root.tex Thu Dec 20 12:23:44 2012 +0000 +++ b/Journal/document/root.tex Thu Dec 20 14:54:06 2012 +0000 @@ -68,7 +68,7 @@ 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. We also generalise the result to the +a solution proposed earlier. We also generalise the 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