--- a/Journal/Paper.thy	Mon Sep 05 13:44:01 2011 +0000
+++ b/Journal/Paper.thy	Mon Sep 05 14:15:32 2011 +0000
@@ -36,7 +36,7 @@
 abbreviation "TIMES \<equiv> Times"
 abbreviation "TIMESS \<equiv> Timess"
 abbreviation "STAR \<equiv> Star"
-abbreviation "ALLREG \<equiv> Allreg"
+abbreviation "ALLS \<equiv> Star Allreg"
 
 definition
   Delta :: "'a lang \<Rightarrow> 'a lang"
@@ -91,7 +91,8 @@
   pderivs_set ("pderss") and
   SUBSEQ ("Subseq") and
   SUPSEQ ("Supseq") and
-  UP ("'(_')\<up>")
+  UP ("'(_')\<up>") and
+  ALLS ("ALL")
   
   
 lemmas Deriv_simps = Deriv_empty Deriv_epsilon Deriv_char Deriv_union
@@ -494,7 +495,7 @@
   rest being in @{term "A\<star>"}. We omit
   the proofs for these properties, but invite the reader to consult our
   formalisation.\footnote{Available in the Archive of Formal Proofs at 
-  \url{http://afp.sf.net/entries/Myhill-Nerode.shtml} 
+  \url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml} 
   \cite{myhillnerodeafp11}.}
 
   The notation in Isabelle/HOL for the quotient of a language @{text A}
@@ -2143,8 +2144,8 @@
 
   \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 infer that every set @{text A} of antichains, namely
+  Higman's Lemma, which is already proved in the Isabelle/HOL library. Higman's
+  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)"}
@@ -2175,16 +2176,15 @@
   \end{lmm}
 
   \begin{proof}
-  Since our alphabet is finite, we can find a regular expression, written @{const Allreg}, that
-  matches every single-character string. With this regular expression we can inductively define
-  the operation @{text "r\<up>"} over regular expressions
+  Since our alphabet is finite, we have a regular expression, written @{text ALL}, that
+  matches every string. With this regular expression we can inductively define
+  the operation @{text "r\<up>"} 
 
   \begin{center}
   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
   @{thm (lhs) UP.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(1)}\\  
   @{thm (lhs) UP.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(2)}\\ 
-  @{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} &\\ 
-   \multicolumn{3}{r}{@{thm (rhs) UP.simps(3)}}\\ 
+  @{thm (lhs) UP.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) UP.simps(3)}\\ 
   @{thm (lhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & 
      @{text "\<equiv>"} & @{thm (rhs) UP.simps(4)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]}\\
   @{thm (lhs) UP.simps(5)[where ?r1.0="r\<^isub>1" and ?r2.0="r\<^isub>2"]} & 
@@ -2194,12 +2194,12 @@
   \end{center}
 
   \noindent
-  and use \eqref{supseqprops} establish that @{thm lang_UP} holds. This shows
-  that @{term "SUBSEQ A"} is regular provided @{text A} is.
+  and use \eqref{supseqprops} to 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 our main lemma, namely
+  Now we can prove our main lemma w.r.t.~@{const "SUPSEQ"}, namely
 
   \begin{lmm}\label{mset}
   For every language @{text A}, there exists a finite language @{text M} such that
@@ -2217,7 +2217,7 @@
   \end{center}
 
   \noindent
-  By Higman's lemma \eqref{higman} we know
+  By Higman's Lemma \eqref{higman} we know
   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
@@ -2236,7 +2236,7 @@
   \noindent
   This lemma allows us to establish the second part of Lemma~\ref{subseqreg}.
 
-  \begin{proof}[The Second Part of Lemma~\ref{subseqreg}]
+  \begin{proof}[Proof of the Second Part of Lemma~\ref{subseqreg}]
   Given any language @{text A}, by Lemma~\ref{mset} we know there exists
   a finite, and thus regular, language @{text M}. We further have @{term "SUPSEQ M = SUPSEQ A"},
   which establishes the second part.    
@@ -2251,9 +2251,9 @@
   \end{equation}
 
   \noindent
-  holds. Now the first part is a simple consequence of the second part.
+  holds. Now the first part of~\ref{subseqreg} is a simple consequence of the second part.
 
-  \begin{proof}[The First Part of Lemma~\ref{subseqreg}]
+  \begin{proof}[Proof of 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 @{term "- SUBSEQ A"} is regular. But since
   we established already that regularity is preserved under complement, also @{term "SUBSEQ A"}
@@ -2419,12 +2419,13 @@
   this to our use of regular expressions, which meant we did not need to `fight' 
   the theorem prover. The code of
   our formalisation can be found in the Archive of Formal Proofs at
-  \mbox{\url{http://afp.sf.net/entries/Myhill-Nerode.shtml}} \cite{myhillnerodeafp11}.\medskip
+  \mbox{\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}} \cite{myhillnerodeafp11}.\medskip
   
   \noindent
   {\bf Acknowledgements:}
   We are grateful for the comments we received from Larry
-  Paulson.
+  Paulson, Tobias Nipkow made us aware of the properties in Lemma~\ref{subseqreg}
+  and Tjark Weber helped us with their proofs.
 
 *}
 

--- a/Journal/document/root.bib	Mon Sep 05 13:44:01 2011 +0000
+++ b/Journal/document/root.bib	Mon Sep 05 14:15:32 2011 +0000
@@ -27,7 +27,7 @@
   title =        {{T}he {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
   booktitle =    {The Archive of Formal Proofs},
   editor =       {G.~Klein and T.~Nipkow and L.~Paulson},
-  publisher =    {\url{http://afp.sf.net/entries/Myhill-Nerode.shtml}},
+  publisher =    {\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}},
   month =        Aug,
   year =         2011,
   note =         {Formal proof development},