diff -r 27270b4bffba -r 73a415af3bcd prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Tue Apr 17 15:37:03 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Apr 17 15:45:05 2012 +0000
@@ -1243,10 +1243,7 @@
   design choices for the PIP scheduler are backed up with a proved
   lemma. We were also able to establish the property that the choice of
   the next thread which takes over a lock is irrelevant for the correctness
-  of PIP. Earlier model checking approaches which verified particular implementations
-  of PIP \cite{Faria08,Jahier09,Wellings07} cannot
-  provide this kind of ``deep understanding'' about the principles behind 
-  PIP and its correctness.
+  of PIP. 
 
   {\bf ??? rewrite the following slightly}