--- a/Journal/Paper.thy	Tue Jul 18 14:46:14 2017 +0100
+++ b/Journal/Paper.thy	Wed Aug 02 13:18:14 2017 +0100
@@ -2049,7 +2049,7 @@
   \end{isabelle}
 
   \noindent This means we need to add a holding edge to the @{text
-  RAG}. However, note while the @{text RAG} changes the corresponding
+  RAG}. However, note that while the @{text RAG} changes the corresponding
   @{text TDG} does not change. Together with the fact that the
   precedences of all threads are unchanged, no @{text cprec} value is
   changed. Therefore, no recalucation of the @{text cprec} value 
@@ -2063,8 +2063,9 @@
   
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm (concl) valid_trace_p_hRAG_s}\\
-  %@ {thm (concl) valid_trace_p_h.eq_cp}
+  @{thm (concl) valid_trace_p_w.RAG_es}\\
+  @{text "If"} @{thm (prem 2) valid_trace_p_w.cp_kept} @{text "then"}
+  @{thm (concl) valid_trace_p_w.cp_kept_tG}
   \end{tabular}
   \end{isabelle}