--- a/Journal/Paper.thy	Wed Aug 24 16:13:20 2016 +0200
+++ b/Journal/Paper.thy	Sun Oct 02 14:32:05 2016 +0100
@@ -403,7 +403,7 @@
   We also use the abbreviation 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm preceds_def}
+  ???%%@  { thm  preceds_def}
   \end{isabelle}
 
   \noindent
@@ -1070,6 +1070,13 @@
   However, we are able to combine their two separate bounds into a
   single theorem improving their bound.
 
+  @{text "th_kept"} shows that th is a thread in s'-s
+
+  \begin{proof}[of Theorem 1]
+  If @{term "th \<in> running (s' @ s)"}, then there is nothing to show. So let us
+  assume otherwise. 
+  \end{proof}
+
   In what follows we will describe properties of PIP that allow us to
   prove Theorem~\ref{mainthm} and, when instructive, briefly describe
   our argument. Recall we want to prove that in state @{term "s' @ s"}