--- a/Journal/Paper.thy	Mon Aug 15 21:09:08 2011 +0000
+++ b/Journal/Paper.thy	Mon Aug 15 22:36:26 2011 +0000
@@ -1568,7 +1568,7 @@
   show that there are only finitely many equivalence classes. So far we 
   showed this directly by induction on @{text "r"} using tagging-functions. 
   However, there is also  an indirect method to come up with such a refined 
-  relation by using derivatives of regular expressions \cite{Brzozowski64}. 
+  relation by using derivatives of regular expressions~\cite{Brzozowski64}. 
 
   Assume the following two definitions for the \emph{left-quotient} of a language,
   which we write as @{term "Der c A"} and @{term "Ders s A"} where @{text c}
@@ -1618,7 +1618,7 @@
   \noindent
   where @{text "\<Delta>"} in the fifth line is a function that tests whether the empty string
   is in the language and returns @{term "{[]}"} or @{term "{}"}, accordingly.
-  The only interesting case above is the last one where we use Prop.~\ref{langprops}@{text "(i)"}
+  The only interesting case is the last one where we use Prop.~\ref{langprops}@{text "(i)"}
   in order to infer that @{term "Der c (A\<star>) = Der c (A \<cdot> A\<star>)"}. We can 
   then complete the proof by noting that @{term "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"}.
   
@@ -1649,7 +1649,8 @@
   The last two clauses extend derivatives from characters to strings---i.e.~list of
   characters. The list-cons operator is written \mbox{@{text "_ :: _"}}. The
   boolean function @{term "nullable r"} needed in the @{const Times}-case tests
-  whether a regular expression can recognise the empty string:
+  whether a regular expression can recognise the empty string. It can be defined as 
+  follows.
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{10mm}}c}
@@ -1670,8 +1671,8 @@
 
   \noindent
   By induction on the regular expression @{text r}, respectively on the string @{text s}, 
-  one can easily show that left-quotients and derivatives relate as follows 
-  \cite{Sakarovitch09}:
+  one can easily show that left-quotients and derivatives of regular expressions 
+  relate as follows (for example \cite{Sakarovitch09}):
 
   \begin{equation}\label{Dersders}
   \mbox{\begin{tabular}{c}
@@ -1681,10 +1682,10 @@
   \end{equation}
 
   \noindent
-  The importance in the context of the Myhill-Nerode theorem is that 
+  The importance of this fact in the context of the Myhill-Nerode theorem is that 
   we can use \eqref{mhders} and \eqref{Dersders} in order to 
   establish that @{term "x \<approx>(lang r) y"} is equivalent to
-  @{term "lang (ders x r) = lang (ders y r)"}. Hence
+  \mbox{@{term "lang (ders x r) = lang (ders y r)"}}. Hence
 
   \begin{equation}
   @{term "x \<approx>(lang r) y"}\hspace{4mm}\mbox{provided}\hspace{4mm}@{term "ders x r = ders y r"}
@@ -1692,20 +1693,21 @@
 
 
   \noindent
-  which means the right-hand side (seen as relation) refines the
-  Myhill-Nerode relation.  Consequently, we can use
-  @{text "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a tagging-relation
-  for the regular expression @{text r}. However, in
-  order to be useful for the second part of the Myhill-Nerode theorem, we also have to show that
-  for the corresponding language there are only finitely many derivatives---thus ensuring
-  that there are only finitely many equivalence classes. Unfortunately, this
-  is not true in general. Sakarovitch gives an example where a regular
-  expression  has infinitely many derivatives w.r.t.~the language
-  \mbox{@{term "({a} \<cdot> {b})\<star> \<union> ({a} \<cdot> {b})\<star> \<cdot> {a}"}}
-  \cite[Page~141]{Sakarovitch09}. 
+  which means the right-hand side (seen as relation) refines the Myhill-Nerode
+  relation.  Consequently, we can use @{text
+  "\<^raw:$\threesim$>\<^bsub>(\<lambda>x. ders x r)\<^esub>"} as a
+  tagging-relation. However, in order to be useful for the second part of the
+  Myhill-Nerode theorem, we have to be able to establish that for the
+  corresponding language there are only finitely many derivatives---thus
+  ensuring that there are only finitely many equivalence
+  classes. Unfortunately, this is not true in general. Sakarovitch gives an
+  example where a regular expression has infinitely many derivatives
+  w.r.t.~the language \mbox{@{term "({a} \<cdot> {b})\<star> \<union> ({a} \<cdot> {b})\<star> \<cdot> {a}"}}
+  \cite[Page~141]{Sakarovitch09}.
+
 
   What Brzozowski \cite{Brzozowski64} established is that for every language there
-  \emph{are} only finitely `dissimilar' derivatives for a regular
+  \emph{are} only finitely `dissimilar' derivatives of a regular
   expression. Two regular expressions are said to be \emph{similar} provided
   they can be identified using the using the @{text "ACI"}-identities:
 
@@ -2050,12 +2052,11 @@
   HOLlight and Isabelle/HOL are based. In order to guarantee consistency,
   formalisations can only extend HOL by definitions that introduce a notion in
   terms of already existing concepts. A convenient definition for automata
-  (based on graphs) use a polymorphic type for the state nodes. This allows us
-  to use the standard operation of disjoint union in order to compose two
-  automata. But we cannot use such a polymorphic definition of automata in HOL
-  as part of the definition for regularity of a language (a set of strings).
-  Consider the following attempt
-
+  (based on graphs) uses a polymorphic type for the state nodes. This allows
+  us to use the standard operation of disjoint union in order to compose two
+  automata. Unfortunately, we cannot use such a polymorphic definition of
+  in HOL as part of the definition for regularity of a language (a
+  set of strings).  Consider the following attempt
 
   \begin{center}
   @{text "is_regular A \<equiv> \<exists>M(\<alpha>). is_finite_automata (M) \<and> \<calL>(M) = A"}