--- a/Correctness.thy	Thu Jan 14 03:29:22 2016 +0000
+++ b/Correctness.thy	Fri Jan 15 02:05:29 2016 +0000
@@ -503,29 +503,29 @@
 qed
 
 text {*
-  The following lemma shows how the counting of 
-  @{term "P"} and @{term "V"} operations affects 
-  the running state of threads in @{term t}.
 
-  The lemma shows that if a thread's @{term "P"}-count equals 
-  its @{term "V"}-count (which means it no longer has any 
-  resource in its possession), it can not be in running thread. 
+  The following lemma shows how the counters for @{term "P"} and
+  @{term "V"} operations relate to the running threads in the states
+  @{term s} and @{term "t @ s"}.  The lemma shows that if a thread's
+  @{term "P"}-count equals its @{term "V"}-count (which means it no
+  longer has any resource in its possession), it cannot be a running
+  thread.
 
-  The proof is by contraction with the assumption @{text "th' \<noteq> th"}. 
-  The key is the use of @{thm count_eq_dependants}
-  to derive the emptiness of @{text th'}s @{term dependants}-set
-  from the balance of its @{term P} @{term V} counts. 
-  From this, it can be shown @{text th'}s @{term cp}-value 
-  equals to its own precedence. 
+  The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
+  The key is the use of @{thm count_eq_dependants} to derive the
+  emptiness of @{text th'}s @{term dependants}-set from the balance of
+  its @{term P} and @{term V} counts.  From this, it can be shown
+  @{text th'}s @{term cp}-value equals to its own precedence.
 
-  On the other hand, since @{text th'} is running, by 
-  @{thm runing_preced_inversion}, its @{term cp}-value
-  equals to the precedence of @{term th}. 
+  On the other hand, since @{text th'} is running, by @{thm
+  runing_preced_inversion}, its @{term cp}-value equals to the
+  precedence of @{term th}.
 
-  Combining the above two we have that @{text th'} and 
-  @{term th} have the same precedence. By uniqueness of precedence, we
-  have @{text "th' = th"}, which is in contradiction with the
-  assumption @{text "th' \<noteq> th"}. 
+  Combining the above two resukts we have that @{text th'} and @{term
+  th} have the same precedence. By uniqueness of precedences, we have
+  @{text "th' = th"}, which is in contradiction with the assumption
+  @{text "th' \<noteq> th"}.
+
 *} 
                       
 lemma eq_pv_blocked: (* ddd *)