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