# HG changeset patch
# User urbanc
# Date 1329089149 0
# Node ID 463bed13070539b9564d7341162b95b1e9ed30ef
# Parent  bd05c5011c0f1d37704e36c29303b35881bde8d5
some polishing

diff -r bd05c5011c0f -r 463bed130705 prio/Paper/Paper.thy
--- 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 *}
diff -r bd05c5011c0f -r 463bed130705 prio/paper.pdf
Binary file prio/paper.pdf has changed