--- a/Journal/Paper.thy	Thu Jan 28 13:46:45 2016 +0000
+++ b/Journal/Paper.thy	Thu Jan 28 14:26:10 2016 +0000
@@ -883,20 +883,26 @@
 
   \begin{theorem}\label{mainthm}
   Given the assumptions about states @{text "s"} and @{text "s' @ s"},
-  the thread @{text th} and the events in @{text "s'"},
-  if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
-  @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and 
-  @{term "cp (s' @ s) th' = prec th s"}.
+  the thread @{text th} and the events in @{text "s'"}, then either
+  \begin{itemize}
+  \item @{term "th \<in> running (s' @ s)"} or\medskip
+
+  \item there exists a thread @{term "th'"} with @{term "th' \<noteq> th"}
+  and @{term "th' \<in> running (s' @ s)"} such that @{text "th' \<in> threads
+  s"}, @{text "\<not> detached s th'"} and @{term "cp (s' @ s) th' = prec
+  th s"}.
+  \end{itemize}
   \end{theorem}
 
   \noindent This theorem ensures that the thread @{text th}, which has
-  the highest precedence in the state @{text s}, can only be blocked
-  in the state @{text "s' @ s"} by a thread @{text th'} that already
-  existed in @{text s} and requested or had a lock on at least one
-  resource---that means the thread was not \emph{detached} in @{text
-  s}.  As we shall see shortly, that means there are only finitely
-  many threads that can block @{text th} in this way and then they
-  need to run with the same precedence as @{text th}.
+  the highest precedence in the state @{text s}, is either running in
+  state @{term "s' @ s"}, or can only be blocked in the state @{text
+  "s' @ s"} by a thread @{text th'} that already existed in @{text s}
+  and requested or had a lock on at least one resource---that means
+  the thread was not \emph{detached} in @{text s}.  As we shall see
+  shortly, that means there are only finitely many threads that can
+  block @{text th} in this way and then they need to run with the same
+  precedence as @{text th}.
 
   Like in the argument by Sha et al.~our finite bound does not
   guarantee absence of indefinite Priority Inversion. For this we