pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:f933a8ad24e5
+:c3a42076b164
 size. Moreover, our result is a good
 witness for one of the major reasons to be interested in machine checked
 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
+is 310 lines long; our graph theory implementation using relations is
-1860 lines; the basic properties of PIP take around 5500 lines of code;
+1615 lines; the basic properties of PIP take around 5000 lines of code;
-and the formal correctness proof 1700 lines.
+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
 %\noindent
 %{\bf Acknowledgements:}