--- a/prio/Paper/Paper.thy	Mon Feb 13 22:17:54 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 22:45:06 2012 +0000
@@ -1186,10 +1186,12 @@
   formal investigation of this is beyond the scope of this paper.
   We are not aware of any proofs in this area, not even informal ones.
  
-  Our formalisation consists of X lines of readable Isabelle/Isar code, with some
-  apply-scripts interspersed. The formal model is Y lines long; the 
-  formal correctness proof Z lines. The properties relevant for an
-  implementation are U lines long.
+  Our formalisation consists of 6894 of readable Isabelle/Isar code, with some
+  apply-scripts interspersed. The formal model is 385 lines long; the 
+  formal correctness proof 3777 lines. The properties relevant for an
+  implementation are 1964 lines long; Auxlliary definitions and notions are 
+  768 lines.
+  
 
 *}