--- a/Journal/Paper.thy	Mon Aug 14 14:16:25 2017 +0100
+++ b/Journal/Paper.thy	Thu Sep 07 16:04:03 2017 +0100
@@ -2357,19 +2357,19 @@
   reasoning: gaining deeper understanding of the subject matter.
 
   Our formalisation
-  consists of around 600 lemmas and overall 10800 lines 
+  consists of around 600 lemmas and overall 9200 lines 
   of readable and commented Isabelle/Isar
   code with a few apply-scripts interspersed. The formal model of PIP
-  is 620 lines long; our graph theory implementation using relations is 
-  1860 lines; the basic properties of PIP take around 5500 lines of code; 
-  and the formal correctness proof 1700 lines. 
+  is 310 lines long; our graph theory implementation using relations is 
+  1615 lines; the basic properties of PIP take around 5000 lines of code; 
+  and the formal correctness proof 1250 lines. 
   %Some auxiliary
   %definitions and proofs span over 770 lines of code. 
   The properties relevant
   for an implementation require 1000 lines. 
   The code of our formalisation 
   can be downloaded from the Mercurial repository at
-  \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/pip}.
+  \url{http://talisker.inf.kcl.ac.uk/cgi-bin/repos.cgi/pip}.
 
   %\medskip