--- a/Journal/Paper.thy	Mon Mar 03 16:22:48 2014 +0000
+++ b/Journal/Paper.thy	Tue Mar 04 08:45:11 2014 +0000
@@ -524,7 +524,7 @@
   \noindent
   where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
   choice for the next waiting list. It just has to be a list of distinctive threads and
-  contain the same elements as @{text "qs"}. This gives for @{term V} the clause:
+  contains the same elements as @{text "qs"}. This gives for @{term V} the clause:
  
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -1018,7 +1018,7 @@
   in PIP is quite ``heavy weight'' in Linux (see the Introduction).
   In our model of PIP the current precedence of a thread in a state @{text s}
   depends on all its dependants---a ``global'' transitive notion,
-  which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).
+  which is indeed heavy weight (see Definition shown in \eqref{cpreced}).
   We can however improve upon this. For this let us define the notion
   of @{term children} of a thread @{text th} in a state @{text s} as
 
@@ -1464,7 +1464,8 @@
   in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who 
   pointed 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 feel confident about the correctness of our results.  
+  invaluable to us in order to be confident about the correctness of our reasoning 
+  (no 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