# HG changeset patch # User urbanc # Date 1299323199 0 # Node ID 1cc87efb3b5346803f04f8fa2e014326fdc644c6 # Parent f1fea2c2713f0f912057bf6fbc51702023191e62 formalisation of first direction is now only 780 loc diff -r f1fea2c2713f -r 1cc87efb3b53 Paper/Paper.thy --- a/Paper/Paper.thy Sat Feb 26 15:44:38 2011 +0000 +++ b/Paper/Paper.thy Sat Mar 05 11:06:39 2011 +0000 @@ -1317,7 +1317,7 @@ Owens and Slind \cite{OwensSlind08}. - Our formalisation consists of 790 lines of Isabelle/Isar code for the first + Our formalisation consists of 780 lines of Isabelle/Isar code for the first direction and 475 for the second, plus around 300 lines of standard material about regular languages. While this might be seen as too large to count as a concise proof pearl, this should be seen in the context of the work done by