--- a/Journal/document/root.tex	Fri Dec 21 00:24:30 2012 +0000
+++ b/Journal/document/root.tex	Fri Dec 21 13:30:14 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 proof to the
+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