--- a/Journal/Paper.thy	Tue May 16 17:20:49 2017 +0100
+++ b/Journal/Paper.thy	Thu May 18 14:30:08 2017 +0100
@@ -1619,8 +1619,8 @@
   s}. Otherwise our PIP scheduler could be ``swamped'' with @{text
   "Create"}-requests.  So our first assumption states:
 
-  \begin{quote} {\bf Assumption on the number of threads created in
-  every valid state after the state {\boldmath@{text s}}:} Given the
+  \begin{quote} {\bf Assumption on the number of threads created 
+  after the state {\boldmath@{text s}}:} Given the
   state @{text s}, in every ``future'' valid state @{text "t @ s"}, we
   require that the number of created threads is less than
   a bound @{text "BC"}, that is 
@@ -1633,7 +1633,7 @@
   "s' @ s"} after @{text s}.  Instead, we need to put this bound on
   the @{text "Create"} events for all valid states after @{text s}.
   This ensures that no matter which ``future'' state is reached, the number
-  of creates is finite.
+  of @{text "Create"}-events is finite.
 
   For our second assumption about giving up resources after a finite
   amount of ``time'', let us introduce the following definition about
@@ -1644,9 +1644,11 @@
   \end{isabelle}
 
   \noindent This set contains all treads that are not detached in
-  state @{text s} (i.e.~they have a lock on a resource) and therefore
-  can potentially block @{text th} after state @{text s}. We need to
-  make the following assumption about the threads in this set:
+  state @{text s}. According to our definiton of @{text "detached"},
+  this means a thread in @{text "blockers"} either holds or waits for
+  some resource. Our Theorem~1 implies that they can all potentially
+  block @{text th} after state @{text s}. We need to make the
+  following assumption about the threads in this set:
 
   \begin{quote}
   {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} 
@@ -1664,20 +1666,19 @@
   s}. The bound reflects how each thread @{text "th'"} is programmed:
   Though we cannot express what instructions a thread is executing,
   the events in our model correspond to the system calls made by
-  thread. Our @{text "BND(th')"} binds the number of these calls.
+  thread. Our @{text "BND(th')"} binds the number of these ``calls''.
   
   The main reason for these two assumptions is that we can prove the
   following: The number of states after @{text s} in which the thread
   @{text th} is not running (that is where Priority Inversion occurs)
   can be bounded by the number of actions the threads in @{text
-  blockers} perform and how many threads are newly created. This bound
-  can be stated for all valid intermediate states @{term "t @ s"} that
-  can happen after @{text s}. To state our bound we need to make a
-  definition of what we mean by intermediate states; it will be the
-  list of states starting from @{text s} upto the state @{text "t @
-  s"}. For example, suppose $\textit{t} = 
-  [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2, \textit{e}_1]$, then
-  the intermediate states from @{text s} upto @{text "t @ s"} are
+  blockers} perform and how many threads are newly created.  To state
+  our bound formally, we need to make a definition of what we mean by
+  intermediate states; it will be the list of states starting from
+  @{text s} upto the state @{text "t @ s"}. For example, suppose
+  $\textit{t} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2,
+  \textit{e}_1]$, then the intermediate states from @{text s} upto
+  @{text "t @ s"} are
 
   \begin{center}
   \begin{tabular}{l}
@@ -1690,7 +1691,8 @@
   \end{center}
 
 
-  \noindent This can be defined by the following recursive function
+  \noindent This list of \emph{intermediate states} can be defined by
+  the following recursive function
 
   \begin{center}
   \begin{tabular}{lcl}

Binary file journal.pdf has changed