# HG changeset patch
# User zhang
# Date 1329173106 0
# Node ID 630754a81bdbafadd9f5ae960d8692000210b77d
# Parent  995515b6f9791fe9710968830f70ae3bb825c021
Line numbers added.

diff -r 995515b6f979 -r 630754a81bdb prio/Paper/Paper.thy
--- 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.
+  
 
 *}
 
diff -r 995515b6f979 -r 630754a81bdb prio/Precedence_ord.thy
--- a/prio/Precedence_ord.thy	Mon Feb 13 22:17:54 2012 +0000
+++ b/prio/Precedence_ord.thy	Mon Feb 13 22:45:06 2012 +0000
@@ -1,7 +1,3 @@
-(*  Title:      HOL/Library/Product_ord.thy
-    Author:     Norbert Voelker
-*)
-
 header {* Order on product types *}
 
 theory Precedence_ord