--- a/Journal/Paper.thy	Tue Apr 25 16:23:46 2017 +0100
+++ b/Journal/Paper.thy	Fri Apr 28 13:20:44 2017 +0100
@@ -413,8 +413,14 @@
   \noindent
   This allows us to define what actions a set of threads @{text ths} might
   perform in a list of events @{text s}, namely
-  @{thm actions_of_def[THEN eq_reflection]}.
-  A \emph{precedence} of a thread @{text th} in a 
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm actions_of_def[where ?s="s" and ?ths="ths", THEN eq_reflection]}.
+  \end{isabelle}
+
+  where we use Isabelle's notation for list-comprehensions. This
+  notation is very similar to notation used in Haskell for list
+  comprehensions.  A \emph{precedence} of a thread @{text th} in a
   state @{text s} is the pair of natural numbers defined as
   
   \begin{isabelle}\ \ \ \ \ %%%
@@ -1118,11 +1124,11 @@
   which is equal to the @{term preced} of @{text th}.\qed
   \end{proof}
 
-  \endnote{
-  @{thm "th_blockedE_pretty"} -- thm-blockedE??
-  
-  @{text "th_kept"} shows that th is a thread in s'-s
-  }
+  %\endnote{
+  %@{thm "th_blockedE_pretty"} -- thm-blockedE??
+  % 
+  % @{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
   hold a resource in state @{text s}.