diff -r 5faa1b59e870 -r 813e7257c7c3 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Thu Feb 16 08:12:01 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 20 11:02:50 2012 +0000
@@ -541,7 +541,7 @@
   \end{center}
 
   \noindent
-  The first rule states that a thread can only be created, if it does not yet exists.
+  The first rule states that a thread can only be created, if it is not alive yet.
   Similarly, the second rule states that a thread can only be terminated if it was
   running and does not lock any resources anymore (this simplifies slightly our model;
   in practice we would expect the operating system releases all locks held by a
@@ -559,7 +559,7 @@
   the responsibility of the programmer.  In our formal
   model we brush aside these problematic cases in order to be able to make
   some meaningful statements about PIP.\footnote{This situation is
-  similar to the infamous occurs check in Prolog: In order to say
+  similar to the infamous \emph{occurs check} in Prolog: In order to say
   anything meaningful about unification, one needs to perform an occurs
   check. But in practice the occurs check is omitted and the
   responsibility for avoiding problems rests with the programmer.}
@@ -602,11 +602,11 @@
   Sha et al.~state their first correctness criterion for PIP in terms
   of the number of low-priority threads \cite[Theorem 3]{Sha90}: if
   there are @{text n} low-priority threads, then a blocked job with
-  high priority can only be blocked @{text n} times.
+  high priority can only be blocked a maximum of @{text n} times.
   Their second correctness criterion is given
   in terms of the number of critical resources \cite[Theorem 6]{Sha90}: if there are
   @{text m} critical resources, then a blocked job with high priority
-  can only be blocked @{text m} times. Both results on their own, strictly speaking, do
+  can only be blocked a maximum of @{text m} times. Both results on their own, strictly speaking, do
   \emph{not} prevent indefinite, or unbounded, Priority Inversion,
   because if a low-priority thread does not give up its critical
   resource (the one the high-priority thread is waiting for), then the
@@ -627,23 +627,26 @@
   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
   reason is that we allow that critical sections can intersect
-  (something Sha et al.~explicitly exclude).  Therefore we have designed a 
-  different correctness criterion for PIP. The idea behind our
-  criterion is as follows: for all states @{text
-  s}, we know the corresponding thread @{text th} with the highest
-  precedence; we show that in every future state (denoted by @{text
-  "s' @ s"}) in which @{text th} is still alive, either @{text th} is
-  running or it is blocked by a thread that was alive in the state
-  @{text s} and was 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. We will actually prove a stronger statement where we also provide
-  the current precedence of the blocking thread. However, this
-  correctness criterion hinges upon a number of assumptions about the
-  states @{text s} and @{text "s' @ s"}, the thread @{text th} and the
-  events happening in @{text s'}. We list them next:
+  (something Sha et al.~explicitly exclude).  Therefore we have
+  designed a different correctness criterion for PIP. The idea behind
+  our criterion is as follows: for all states @{text s}, we know the
+  corresponding thread @{text th} with the highest precedence; we show
+  that in every future state (denoted by @{text "s' @ s"}) in which
+  @{text th} is still alive, either @{text th} is running or it is
+  blocked by a thread that was alive in the state @{text s} and was 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 priority are created in @{text "s'"}. We will actually prove a
+  stronger statement where we also provide the current precedence of
+  the blocking thread. However, this correctness criterion hinges upon
+  a number of assumptions about the states @{text s} and @{text "s' @
+  s"}, the thread @{text th} and the events happening in @{text
+  s'}. We list them next:
 
   \begin{quote}
-  {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make 
+  {\bf Assumptions on the states {\boldmath@{text s}} and 
+  {\boldmath@{text "s' @ s"}:}} In order to make 
   any meaningful statement, we need to require that @{text "s"} and 
   @{text "s' @ s"} are valid states, namely
   \begin{isabelle}\ \ \ \ \ %%%
@@ -655,7 +658,8 @@
   \end{quote}
 
   \begin{quote}
-  {\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be alive in @{text s} and 
+  {\bf Assumptions on the thread {\boldmath@{text "th"}:}} 
+  The thread @{text th} must be alive in @{text s} and 
   has the highest precedence of all alive threads in @{text s}. Furthermore the
   priority of @{text th} is @{text prio} (we need this in the next assumptions).
   \begin{isabelle}\ \ \ \ \ %%%
@@ -668,7 +672,7 @@
   \end{quote}
   
   \begin{quote}
-  {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot
+  {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot
   be blocked indefinitely. Of course this can happen if threads with higher priority
   than @{text th} are continuously created in @{text s'}. Therefore we have to assume that  
   events in @{text s'} can only create (respectively set) threads with equal or lower 
@@ -686,7 +690,7 @@
 
   \noindent
   The locale mechanism of Isabelle helps us to manage conveniently such assumptions~\cite{Haftmann08}.
-  Under these assumptions we will prove the following correctness property:
+  Under these assumptions we shall prove the following correctness property:
 
   \begin{theorem}\label{mainthm}
   Given the assumptions about states @{text "s"} and @{text "s' @ s"},
@@ -808,7 +812,7 @@
   that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the 
   precedence of @{text th} in @{text "s"}.
   We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
-  This theorem gives a stricter bound on the processes that can block @{text th} than the
+  This theorem gives a stricter bound on the threads that can block @{text th} than the
   one obtained by Sha et al.~\cite{Sha90}:
   only threads that were alive in state @{text s} and moreover held a resource.
   This means our bound is in terms of both---alive threads in state @{text s}
@@ -1229,7 +1233,7 @@
   to \cite{Steinberg10}, is that except for one unsatisfactory
   proposal nobody has a good idea for how PIP should be modified to
   work correctly on multi-processor systems. The difficulties become
-  clear when considering the fact that locking and releasing a resource always
+  clear when considering the fact that releasing and re-locking a resource always
   requires a small amount of time. If processes work independently,
   then a low priority process can ``steal'' in such an unguarded
   moment a lock for a resource that was supposed to allow a high-priority