--- a/Journal/Paper.thy	Fri Apr 28 13:20:44 2017 +0100
+++ b/Journal/Paper.thy	Fri Apr 28 15:05:36 2017 +0100
@@ -166,7 +166,7 @@
   Yodaiken \cite{Yodaiken02} and also Moylan et
   al.~\cite{deinheritance} point to a subtlety that had been
   overlooked in the informal proof by Sha et al. They specify PIP in
-  \cite{Sha90} so that after the thread (whose priority has been
+  \cite[Section III]{Sha90} so that after the thread (whose priority has been
   raised) completes its critical section and releases the lock, it
   ``{\it returns to its original priority level}''. This leads them to
   believe that an implementation of PIP is ``{\it rather
@@ -812,17 +812,19 @@
   \end{tabular}
   \end{isabelle}
 
-  \noindent
-  %%In the second definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
-  Note that in the initial state, that is where the list of events is empty, the set 
-  @{term threads} is empty and therefore there is neither a thread ready nor running.
-  If there is one or more threads ready, then there can only be \emph{one} thread
-  running, namely the one whose current precedence is equal to the maximum of all ready 
-  threads. We use sets to capture both possibilities.
-  We can now also conveniently define the set of resources that are locked by a thread in a
-  given state and also when a thread is detached in a state (meaning the thread neither 
-  holds nor waits for a resource---in the RAG this would correspond to an
-  isolated node without any incoming and outgoing edges, see Figure~\ref{RAGgraph}):
+  \noindent In the second definition @{term "DUMMY ` DUMMY"} stands
+  for the image of a set under a function.  Note that in the initial
+  state, that is where the list of events is empty, the set @{term
+  threads} is empty and therefore there is neither a thread ready nor
+  running.  If there is one or more threads ready, then there can only
+  be \emph{one} thread running, namely the one whose current
+  precedence is equal to the maximum of all ready threads. We use sets
+  to capture both possibilities.  We can now also conveniently define
+  the set of resources that are locked by a thread in a given state
+  and also when a thread is detached in a state (meaning the thread
+  neither holds nor waits for a resource---in the RAG this would
+  correspond to an isolated node without any incoming and outgoing
+  edges, see Figure~\ref{RAGgraph}):
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -993,7 +995,8 @@
   possesses locks to two resources for which two high-priority threads
   are waiting for, then lowering the priority prematurely after giving
   up only one lock, can cause indefinite Priority Inversion for one of
-  the high-priority threads, invalidating their two bounds.
+  the high-priority threads, invalidating their two bounds (recall the 
+  counter example described in the Introduction).
 
   Even when fixed, their proof idea does not seem to go through for
   us, because of the way we have set up our formal model of PIP.  One
@@ -1009,7 +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 times. This is independent of how many threads of lower
+  number of threads. This is independent of how many threads of lower
   priority are created in @{text "s'"}. We will actually prove a
   stronger statement where we also provide the current precedence of
   the blocking thread.