--- a/Journal/Paper.thy	Thu Dec 06 16:32:03 2012 +0000
+++ b/Journal/Paper.thy	Wed Dec 12 11:45:04 2012 +0000
@@ -382,7 +382,7 @@
   Because of these problems to do with representing automata, formalising 
   automata theory is surprisingly not as easy as one might think, despite the 
   sometimes very detailed, but informal, textbook proofs. \citeN{LammichTuerk12}
-  formalised Hopcroft's algorithm using an automata library of 27 kloc in
+  formalised Hopcroft's algorithm using an automata library of 14 kloc in
   Isabelle/HOL. There they use matrices for representing automata. 
   Functions are used by \citeN{Nipkow98}, who establishes
   the link between regular expressions and automata in the context of