diff -r 8a9767ab6415 -r 9756a51f2223 Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Feb 20 13:08:04 2017 +0000
+++ b/Journal/Paper.thy	Mon Feb 20 15:53:22 2017 +0000
@@ -1522,37 +1522,49 @@
 
 section {* A Finite Bound on Priority Inversion *}
 
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
 text {*
 
-  Like in the argument by Sha et al.~our result does not
-  yet guarantee absence of indefinite Priority Inversion. For this we
-  further have to assume that every thread gives up its resources
-  after a finite amount of time. We found that this assumption is not
-  so straightforward to formalise in our model. There are mainly two
+  Like in the argument by Sha et al.~our result does not yet guarantee
+  absence of indefinite Priority Inversion. For this we further have
+  to assume that every thread gives up its resources after a finite
+  amount of time. We found that this assumption is not so
+  straightforward to formalise in our model. There are mainly two
   reasons for this: First, we do not specify what ``running'' the code
   of a thread means, for example by giving an operational semantics
   for machine instructions. Therefore we cannot characterise what are
   ``good'' programs that contain for every looking request also a
-  corresponding unlocking request for a resource. Second, we would
-  need to specify a kind of global clock that tracks the time how long
-  a thread locks a resource. But this seems difficult, because how do
-  we conveniently distinguish between a thread that ``just'' locks a
-  resource for a very long time and one that locks it forever.
+  corresponding unlocking request for a resource.  Second, we can
+  distinghish between a thread that ``just'' locks a resource for a
+  finite amount of time (even if it is very long) and one that locks
+  it forever. But this seems difficut.
 
   Therefore we decided in our earlier paper \cite{ZhangUrbanWu12} to
   leave out this property and let the programmer assume the
   responsibility to program threads in such a benign manner (in
   addition to causing no circularity in the RAG). However, in this
-  paper we can make an improvement: 
+  paper we can make an improvement: we can look at the \emph{events}
+  that are happening once a Priority Inversion occurs. The events can
+  be seen as a rough abstraction of the ``runtime behaviour'' of
+  threads and also as an abstract notion for ``time''.  We can then
+  prove a more direct result for the absence of indefinite Priority
+  Inversion. For this let us introduce the following definition:
 
-In this detail, we
-  do not make any progress in comparison with the work by Sha et al.
-  However, we are able to combine their two separate bounds into a
-  single theorem improving their bound. We can characterise a 
-  program
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm blockers_def}
+  \end{isabelle}
+
+  \noindent This set contains all treads that can potentially block
+  @{text th} after state @{text s}.
+
 
 *}
-
+(*<*)
+end
+(*>*)
 
 section {* Properties for an Implementation\label{implement} *}