diff -r 0781a2fc93f1 -r 66ed924aaa5c Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Jun 03 15:00:12 2014 +0100
+++ b/Journal/Paper.thy	Mon Jun 09 16:01:28 2014 +0100
@@ -152,9 +152,12 @@
   \cite[Section 2.3.1]{book} which specifies for a process that 
   inherited a higher priority and exits a critical section ``{\it it resumes 
   the priority it had at the point of entry into the critical section}''.
+  The same error can also be found in the more recent textbook 
+  \cite[Page 119]{Laplante11} which states ``{\it when [the task] exits the critical 
+  section that caused the block, it reverts to the priority it had when 
+  it entered that section}''.
    
-  While \cite{book} and
-  \cite{Sha90} are the only formal publications we have 
+  While \cite{Laplante11,book,Sha90} are the only formal publications we have 
   found that describe the incorrect behaviour, not all, but many
   informal\footnote{informal as in ``found on the Web''} 
   descriptions of PIP overlook the possibility that another
@@ -1564,7 +1567,7 @@
   points out an error in a paper about Preemption 
   Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was
   invaluable to us in order to be confident about the correctness of our reasoning 
-  (no case can be overlooked).   
+  (for example no corner case can be overlooked).   
   The most closely related work to ours is the formal verification in
   PVS of the Priority Ceiling Protocol done by Dutertre
   \cite{dutertre99b}---another solution to the Priority Inversion