--- a/Journal/Paper.thy	Mon Sep 05 13:09:38 2011 +0000
+++ b/Journal/Paper.thy	Mon Sep 05 13:43:12 2011 +0000
@@ -2109,11 +2109,11 @@
   r))"}}. Thus the regular expression @{term "\<Uplus>(pderivs_lang B r)"} verifies that
   @{term "Deriv_lang B A"} is regular.
 
-  Even more surprising is the fact that for every language @{text A}, the language
+  Even more surprising is the fact that for \emph{every} language @{text A}, the language
   consisting of all substrings of @{text A} is regular \cite{Shallit08, Gasarch09}. 
   A substring can be obtained
   by striking out zero or more characters from a string. This can be defined 
-  inductively by the following three rules:
+  inductively in Isabelle/HOL by the following three rules:
 
   \begin{center}
   @{thm[mode=Axiom] emb0[where bs="x"]}\hspace{10mm} 
@@ -2123,7 +2123,8 @@
 
   \noindent
   It can be easily proved that @{text "\<preceq>"} is a partial order. Now define the 
-  language of substrings and superstrings of a language @{text A}:
+  \emph{language of substrings} and \emph{superstrings} of a language @{text A} 
+  respectively as
 
   \begin{center}
   \begin{tabular}{l}
@@ -2136,14 +2137,14 @@
   We like to establish
 
   \begin{lmm}\label{subseqreg}
-  For any language @{text A}, the languages @{term "SUBSEQ A"} and @{term "SUPSEQ A"}
+  For every language @{text A}, the languages @{term "SUBSEQ A"} and @{term "SUPSEQ A"}
   are regular.
   \end{lmm}
 
   \noindent
   Our proof follows the one given in \cite[92--95]{Shallit08}, except that we use
   Higman's lemma, which is already proved in the Isabelle/HOL library. Higman's
-  lemma allows us to prove that every set @{text A} of antichains, namely
+  lemma allows us to infer that every set @{text A} of antichains, namely
 
   \begin{equation}\label{higman}
   @{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"}
@@ -2152,7 +2153,7 @@
   \noindent
   is finite.
 
-  It is straightforward to prove the following properties of @{term SUPSEQ}
+  The first step in our proof is to establish the following properties for @{term SUPSEQ}
 
   \begin{equation}\label{supseqprops}
   \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
@@ -2170,7 +2171,7 @@
   empty string. With these properties at our disposal we can establish the lemma
 
   \begin{lmm}
-  If @{text A} is regular, then also @{term "SUBSEQ A"}.
+  If @{text A} is regular, then also @{term "SUPSEQ A"}.
   \end{lmm}
 
   \begin{proof}
@@ -2192,12 +2193,12 @@
   \end{center}
 
   \noindent
-  and using \eqref{supseqprops} establish that @{thm lang_UP}. This shows
+  and use \eqref{supseqprops} establish that @{thm lang_UP} holds. This shows
   that @{term "SUBSEQ A"} is regular provided @{text A} is.
   \end{proof}
 
   \noindent
-  Now we can prove the main lemma, namely
+  Now we can prove our main lemma, namely
 
   \begin{lmm}\label{mset}
   For every language @{text A}, there exists a finite language @{text M} such that
@@ -2208,7 +2209,7 @@
 
   \begin{proof}
   For @{text M} we take the set of all minimal elements of @{text A}. An element @{text x} 
-  is minimal in @{text A} provided
+  is said to be \emph{minimal} in @{text A} provided
 
   \begin{center}
   @{thm minimal_def}
@@ -2216,7 +2217,7 @@
 
   \noindent
   By Higman's lemma \eqref{higman} we know
-  that @{text "M"} is finite, since every minimal element is incomparable, 
+  that @{term "M \<equiv> {x \<in> A. minimal x A}"} is finite, since every minimal element is incomparable, 
   except with itself.
   It is also straightforward to show that @{term "SUPSEQ M \<subseteq> SUPSEQ A"}. For
   the other direction we have  @{term "x \<in> SUPSEQ A"}. From this we can obtain 
@@ -2226,9 +2227,9 @@
   and hence by transitivity also \mbox{@{term "z \<preceq> x"}} (here we deviate from the argument 
   given in \cite{Shallit08}, because Isabelle/HOL provides already an extensive infrastructure
   for reasoning about well-foundedness). Since @{term "z"} is
-  minimal and in @{term A}, we also know that @{term z} is in @{term M}.
+  minimal and an element in @{term A}, we also know that @{term z} is in @{term M}.
   From this together with @{term "z \<preceq> x"}, we can infer that @{term x} is in 
-  @{term "SUPSEQ M"} as required.
+  @{term "SUPSEQ M"}, as required.
   \end{proof}
 
   \noindent
@@ -2241,16 +2242,19 @@
   \end{proof}
 
   \noindent
-  In order to establish the first part of Lemma~\ref{subseqreg} we use the
-  property proved in \cite{Shallit08}
+  In order to establish the first part of Lemma~\ref{subseqreg}, we use the
+  property proved in \cite{Shallit08}, namely that
 
   \begin{equation}\label{compl}
   @{thm SUBSEQ_complement}
   \end{equation}
 
+  \noindent
+  holds. Now the first part is a simple consequence of the second part.
+
   \begin{proof}[The First Part of Lemma~\ref{subseqreg}]
   By the second part of Lemma~\ref{subseqreg}, we know the right-hand side of \eqref{compl}
-  is regular, which means the complement of @{term "SUBSEQ A"} is regular. But since
+  is regular, which means @{term "- SUBSEQ A"} is regular. But since
   we established already that regularity is preserved under complement, also @{term "SUBSEQ A"}
   must be regular. 
   \end{proof}