--- a/prio/Paper/Paper.thy	Mon Apr 16 08:48:20 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Apr 16 12:54:08 2012 +0000
@@ -93,7 +93,7 @@
   implemented. This includes VxWorks (a proprietary real-time OS used
   in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
   ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
-  example in libraries for FreeBSD, Solaris and Linux.
+  example in libraries for FreeBSD, Solaris and Linux. ({\bf Is this True?})
 
   One advantage of PIP is that increasing the priority of a thread
   can be dynamically calculated by the scheduler. This is in contrast
@@ -167,14 +167,16 @@
   into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
   checking techniques. This paper presents a formalised and
   mechanically checked proof for the correctness of PIP (to our
-  knowledge the first one; the earlier informal proof by Sha et
-  al.~\cite{Sha90} is flawed).  In contrast to model checking, our
+  knowledge the first one). 
+  %; the earlier informal proof by Sha et
+  %al.~\cite{Sha90} is flawed).  
+  In contrast to model checking, our
   formalisation provides insight into why PIP is correct and allows us
   to prove stronger properties that, as we will show, can inform an
   efficient implementation.  For example, we found by ``playing'' with the formalisation
   that the choice of the next thread to take over a lock when a
   resource is released is irrelevant for PIP being correct---a fact
-  that has not been mentioned in the relevant literature.
+  that has not been mentioned in the literature.
 *}
 
 section {* Formal Model of the Priority Inheritance Protocol *}