diff -r a821434474c9 -r 541bfdf1fa36 prio/Paper/document/root.tex
--- a/prio/Paper/document/root.tex	Wed Feb 01 17:46:36 2012 +0000
+++ b/prio/Paper/document/root.tex	Thu Feb 02 13:58:16 2012 +0000
@@ -37,8 +37,7 @@
 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}
 \begin{document}
 
-\title{A Formalisation of Priority Inheritance Protocol \\ 
-       for Correct and Efficient Implementation}
+\title{Priority Inheritance Protocol Proved Correct}
 \author{Xingyuan Zhang\inst{1} \and Christian Urban\inst{2} \and Chunhan Wu\inst{1}}
 \institute{PLA University of Science and Technology, China \and 
            King's College London, United Kingdom}
@@ -57,7 +56,7 @@
 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
+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.\medskip