--- a/Journal/Paper.thy	Fri May 05 14:26:00 2017 +0100
+++ b/Journal/Paper.thy	Fri May 05 14:53:56 2017 +0100
@@ -1093,39 +1093,39 @@
   block @{text th} in this way.
 
   
-%% HERE
+  %% HERE
 
-  Given our assumptions (on @{text th}), the first property we can
-  show is that any running thread, say @{text "th'"}, has the same
-  precedence as @{text th}:
+  %Given our assumptions (on @{text th}), the first property we can
+  %show is that any running thread, say @{text "th'"}, has the same
+  %precedence as @{text th}:
 
-  \begin{lemma}\label{runningpreced}
-  @{thm [mode=IfThen] running_preced_inversion}
-  \end{lemma}
+  %\begin{lemma}\label{runningpreced}
+  %@{thm [mode=IfThen] running_preced_inversion}
+  %\end{lemma}
 
-  \begin{proof}
-  By definition, the running thread has as current precedence the maximum of
-  all ready threads, that is
+  %\begin{proof}
+  %By definition, the running thread has as current precedence the maximum of
+  %all ready threads, that is
 
-  \begin{center}
-  @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"}
-  \end{center}
+  %\begin{center}
+  %@{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"}
+  %\end{center}
 
-  \noindent
-  We also know that this is equal to the maximum of current precedences of all threads,
-  that is
+  %\noindent
+  %We also know that this is equal to the maximum of current precedences of all threads,
+  %that is
 
-  \begin{center}
-  @{term "cp (t @ s) th' = Max (cp (t @ s) ` threads (t @ s))"}
-  \end{center}
+  %\begin{center}
+  %@{term "cp (t @ s) th' = Max (cp (t @ s) ` threads (t @ s))"}
+  %\end{center}
 
-  \noindent
-  This is because each ready thread, say @{text "th\<^sub>r"}, has the maximum
-  current precedence of the subtree located at @{text "th\<^sub>r"}. All these
-  subtrees together form the set of threads.
-  But the maximum of all threads is the @{term "cp"} of @{text "th"},
-  which is equal to the @{term preced} of @{text th}.\qed
-  \end{proof}
+  %\noindent
+  %This is because each ready thread, say @{text "th\<^sub>r"}, has the maximum
+  %current precedence of the subtree located at @{text "th\<^sub>r"}. All these
+  %subtrees together form the set of threads.
+  %But the maximum of all threads is the @{term "cp"} of @{text "th"},
+  %which is equal to the @{term preced} of @{text th}.\qed
+  %\end{proof}
 
   %\endnote{
   %@{thm "th_blockedE_pretty"} -- thm-blockedE??
@@ -1133,7 +1133,7 @@
   % @{text "th_kept"} shows that th is a thread in s'-s
   % }
 
-  Next we show that a running thread @{text "th'"} must either wait for or
+  Given our assumptions (on @{text th}), the first property we show that a running thread @{text "th'"} must either wait for or
   hold a resource in state @{text s}.
 
   \begin{lemma}\label{notdetached}
@@ -1175,17 +1175,12 @@
   in its subtrees (with @{text "th"} having the highest of all threads
   and being in the subtree of @{text "th'"}).  We also have that @{term
   "th \<noteq> th'"} since we assumed @{text th} is not running.
-
   By
   Lem.~\ref{notdetached} we have that @{term "\<not>detached s th'"}.
   If @{text "th'"} is not detached in @{text s}, that is either
   holding or waiting for a resource, it must be that @{term "th' \<in>
-  threads s"}.  By Lem.~\ref{runningpreced} we have
-
-  \begin{center}
-  @{term "cp (t @ s) th' = preced th s"}
-  \end{center}
-
+  threads s"}.\medskip
+  
   \noindent
   This concludes the proof of Theorem 1.\qed
   \end{proof}

Binary file journal.pdf has changed