diff -r 289e362f7a76 -r 389ef8b1959c Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Oct 07 14:05:08 2016 +0100
+++ b/Journal/Paper.thy	Fri Oct 07 21:15:35 2016 +0100
@@ -403,7 +403,7 @@
   We also use the abbreviation 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  ???%%@  { thm  preceds_def}
+  @{abbrev "preceds ths s"}
   \end{isabelle}
 
   \noindent
@@ -1087,6 +1087,17 @@
   \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 all threads, that is
+
+  \begin{center}
+  @{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"}
+  \end{center}
+
+  \noindent
+  But the maximum of all threads is the @{term "cp"} of @{text "th"},
+  which is the @{term preced} of @{text th}.
   \end{proof}
 
   @{thm "th_blockedE_pretty"} -- thm-blockedE??