# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1495548648 -3600
# Node ID 170e59f2d6456472e580f1c0e74d33181183b160
# Parent  1b72810a2d61fd6205391ac8838a2a43a435cbb0
updated

diff -r 1b72810a2d61 -r 170e59f2d645 Journal/Paper.thy
--- a/Journal/Paper.thy	Tue May 23 15:08:47 2017 +0100
+++ b/Journal/Paper.thy	Tue May 23 15:10:48 2017 +0100
@@ -1777,7 +1777,7 @@
   \end{proof}
 
   \noindent This theorem is the main conclusion we obtain for the
-  Priority Inheritance Protocol: it shows that set of @{text blockers}
+  Priority Inheritance Protocol: it shows that the set of @{text blockers}
   is fixed at state @{text s} when @{text th} becomes the thread with
   highest priority. Then no additional blocker of @{text th} can
   appear after the state @{text s}. And in this way we can bound the
diff -r 1b72810a2d61 -r 170e59f2d645 journal.pdf
Binary file journal.pdf has changed