# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1504796643 -3600
# Node ID c3a42076b1648e44a2328031f02ec92912ad6d6c
# Parent  f933a8ad24e59ddec13fc1da69c9d105d390e991
polishing

diff -r f933a8ad24e5 -r c3a42076b164 Journal/Paper.thy
--- 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
 
diff -r f933a8ad24e5 -r c3a42076b164 journal.pdf
Binary file journal.pdf has changed