--- a/Paper/Paper.thy	Sat Feb 19 21:49:11 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 22:05:22 2011 +0000
@@ -1058,28 +1058,28 @@
   regular expression.
 
   While regular expressions are convenient in formalisations, they have some
-  limitations. One is that there seems to be no notion of a minimal regular
-  expression, like there is for automata. For an implementation of a simple
-  regular expression matcher, whose correctness has been formally
-  established, we refer the reader to Owens and Slind \cite{OwensSlind08}.
+  limitations. One is that there seems to be no method of calculating a
+  minimal regular expression (for example in terms of length), like there is
+  for automata. For an implementation of a simple regular expression matcher,
+  whose correctness has been formally established, we refer the reader to
+  Owens and Slind \cite{OwensSlind08}.
 
 
   Our formalisation consists of 790 lines of Isabelle/Isar code for the first
-  direction and 475 for the second, plus 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 Constable at al \cite{Constable00} who formalised the
-  Myhill-Nerode theorem in Nuprl using automata. 
-  They write that their
-  four-member team needed something on the magnitute of 18 months for their
-  formalisation. The estimate for our formalisation is that we
-  needed approximately 3 months and this included the time to find our proof
-  arguments. Unlike Constable et al, who were able to follow the proofs from
-  \cite{HopcroftUllman69}, we had to find our own arguments.  So for us the formalisation
-  was not the bottleneck. It is hard to gauge the size of a formalisation in
-  Nurpl, but from what is shown in the Nuprl Math Library about their
-  development it seems substantially larger than ours. The code of
-  ours can be found in the Mercurial Repository at
+  direction and 475 for the second, plus 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
+  Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem
+  in Nuprl using automata. They write that their four-member team needed
+  something on the magnitute of 18 months for their formalisation. The
+  estimate for our formalisation is that we needed approximately 3 months and
+  this included the time to find our proof arguments. Unlike Constable et al,
+  who were able to follow the proofs from \cite{HopcroftUllman69}, we had to
+  find our own arguments.  So for us the formalisation was not the
+  bottleneck. It is hard to gauge the size of a formalisation in Nurpl, but
+  from what is shown in the Nuprl Math Library about their development it
+  seems substantially larger than ours. The code of ours can be found in the
+  Mercurial Repository at
 
   \begin{center}
   \url{http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/regexp/}
@@ -1108,7 +1108,7 @@
   generated with respect to @{text s}.  Using the fact that two strings are
   Myhill-Nerode related whenever their derivative is the same together with
   the fact that there are only finitely many derivatives for a regular
-  expression would give us the same argument as ours. However it seems not so easy to
+  expression would give us a similar argument as ours. However it seems not so easy to
   calculate the derivatives and then to count them. Therefore we preferred our
   direct method of using tagging-functions involving equivalence classes. This
   is also where our method shines, because we can completely side-step the