--- a/prio/Paper/Paper.thy	Sun Feb 12 23:20:06 2012 +0000
+++ b/prio/Paper/Paper.thy	Sun Feb 12 23:25:49 2012 +0000
@@ -154,13 +154,14 @@
   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; an earlier informal proof by Sha et
+  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, inform an
   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.
+  resource is released is irrelevant for PIP being correct. Something
+  which has not been mentioned in the relevant literature.
 *}
 
 section {* Formal Model of the Priority Inheritance Protocol *}