# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1493732572 -3600
# Node ID f73b7f339314ee63b0b9e184a56ca6156ab2b0c4
# Parent  613189244e723ea201547f98a79d8b56a1c56180
updated

diff -r 613189244e72 -r f73b7f339314 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Apr 28 15:05:36 2017 +0100
+++ b/Journal/Paper.thy	Tue May 02 14:42:52 2017 +0100
@@ -667,7 +667,7 @@
   threads, we deal correctly with the problem in the informal
   algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
   lowered prematurely (see Introduction). We again introduce an abbreviation for current
-  precedeces of a set of threads, written @{term "cprecs wq s ths"}.
+  precedeces of a set of threads, written @{text "cpreceds wq s ths"}.
   
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm cpreceds_def}
@@ -1012,8 +1012,7 @@
   state @{text s} and was waiting for or in the possession of a lock
   in @{text s}. Since in @{text s}, as in every state, the set of
   alive threads is finite, @{text th} can only be blocked a finite
-  number of threads. This is independent of how many threads of lower
-  priority are created in @{text "s'"}. We will actually prove a
+  number of threads.  We will actually prove a
   stronger statement where we also provide the current precedence of
   the blocking thread. 
 
diff -r 613189244e72 -r f73b7f339314 journal.pdf
Binary file journal.pdf has changed