diff -r da7a6ccfa7a9 -r 6b1141c5e24c Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Mar 04 15:30:24 2014 +0000
+++ b/Journal/Paper.thy	Tue Mar 04 15:49:36 2014 +0000
@@ -155,7 +155,7 @@
   \cite[Section 2.3.1]{book} which specifies for a process that 
   inherited a higher priority and exits a critical section ``it resumes 
   the priority it had at the point of entry into the critical section''.
-  
+   
   While \cite{book} and
   \cite{Sha90} are the only formal publications we have 
   found that describe the incorrect behaviour, not all, but many
@@ -1467,9 +1467,9 @@
   for future work.
 
   To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult
-  if done informally by ``pencil-and-paper''. This is proved by the flawed proof
-  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 
+  if done informally by ``pencil-and-paper''. We infer this from the flawed proof
+  in the paper by Sha et al.~\cite{Sha90} and also from \cite{Regehr} where Regehr 
+  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).   
@@ -1494,7 +1494,7 @@
   for an implementation require 2000 lines. 
   The code of our formalisation 
   can be downloaded from the Mercurial repository at
-  \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.
+  \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/pip}.
 
   %\medskip