diff -r 4e0bc10f7907 -r 32985f93e845 Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Jul 11 17:01:50 2017 +0100
+++ b/Journal/Paper.thy	Fri Jul 14 15:08:39 2017 +0100
@@ -1832,8 +1832,8 @@
   of @{term children} of a thread @{text th} (defined in \eqref{children})
   where a child is a thread that is only one ``hop'' away from the thread
   @{text th} in the @{term TDG} (and waiting for @{text th} to release
-  a resource). Using children, we can prove the following lemma for calculating
-  @{text cprec}.
+  a resource). Using children, we can prove the following lemma for more efficiently calculating
+  @{text cprec} of a thread @{text th}.
 
 
   \begin{lemma}\label{childrenlem}
@@ -1845,13 +1845,19 @@
   
   \noindent
   That means the current precedence of a thread @{text th} can be
-  computed locally by considering only the static precedence of @{text th}
+  computed by considering the static precedence of @{text th}
   and 
-  the current precedences of the children of @{text th}. In
-  effect, it only needs to be recomputed for @{text th} when its static
-  precedence is re-set or when one of
-  its children changes its current precedence.  This is much more efficient 
-  because when the  @{text cprec}-value is not changed for a child, 
+  the current precedences of the children of @{text th}. Their 
+  @{text "cprec"}s, in general general, need to be computed by recursively decending into 
+  deeper ``levels'' of the @{text TDG}. 
+  However, the current precedence of a thread @{text th}, say, 
+  only needs to be recomputed when @{text "(i)"} its static
+  precedence is re-set or when @{text "(ii)"} one of
+  its children changes its current precedence or when @{text "(iii)"} the children set changes
+  (for example in an @{text "V"}-event).   
+  If only the static precedence or the children-set changes, the we can 
+  avoid the recursion and compute the @{text cprec} of @{text th} locally.
+  In this cases
   the recursion does not need to decend into the corresponding subtree.
   Once the current 
   precedence is computed in this more efficient manner, the selection