diff -r 1baf8d0c7093 -r 70395e3fd99f prio/Paper/document/root.tex
--- a/prio/Paper/document/root.tex	Mon Jan 30 08:45:56 2012 +0000
+++ b/prio/Paper/document/root.tex	Mon Jan 30 08:55:27 2012 +0000
@@ -54,14 +54,13 @@
 has never been formally verified in a theorem prover. As already
 pointed out in the literature, the original informal investigation of
 the Property Inheritance Protocol presents a correctness ``proof'' for
-an \emph{incorrect} algorithm. In this paper we fix the problem of the
-original proof by making all notions precise and implementing a
-variant of a solution proposed earlier. Our formalisation in
-Isabelle/HOL uncovered 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.\medskip
+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
+uncovered 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.\medskip
 
 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 
 realtime systems