# HG changeset patch
# User urbanc
# Date 1334677505 0
# Node ID 73a415af3bcd60378181e178a23f3b83e167d02b
# Parent  27270b4bffba9ea923ea052a9773fd684c1fa845
some small tuning

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}
 
diff -r 27270b4bffba -r 73a415af3bcd prio/paper.pdf
Binary file prio/paper.pdf has changed