--- a/Journal/Paper.thy	Thu Sep 12 10:34:11 2013 +0200
+++ b/Journal/Paper.thy	Thu Sep 12 17:20:48 2013 +0100
@@ -332,17 +332,19 @@
 
   \noindent
   changes the type---the disjoint union is not a set, but a set of
-  pairs. Using this definition for disjoint union means we do not have a
-  single type for the states of automata. As a result we will not be able to
-  define a regular language as one for which there exists
-  an automaton that recognises all its strings (Definition~\ref{baddef}). This
-  is because we cannot make a definition in HOL that is only polymorphic in
-  the state type, but not in the predicate for regularity; and there is no
-  type quantification available in HOL (unlike in Coq, for
-  example).\footnote{Slind already pointed out this problem in an email to the
-  HOL4 mailing list on 21st April 2005.}
-  %$^,$\footnote{While in Coq one can avoid 
-  %this particular problem, all other difficulties we point out below still apply.}
+  pairs. Using this definition for disjoint union means we do not have
+  a single type for the states of automata. As a result we will not be
+  able to define a regular language as one for which there exists an
+  automaton that recognises all its strings
+  (Definition~\ref{baddef}). This is because we cannot make a
+  definition in HOL that is only polymorphic in the state type, but
+  not in the predicate for regularity; and there is no type
+  quantification available in HOL.\footnote{Slind already pointed out
+  this problem in an email to the HOL4 mailing list on 21st April
+  2005.} Coq, for example, has quantification over types and thus can
+  state such a definition.  This has been recently exploited in a
+  slick formalisation of the Myhill-Nerode theorem in Coq by
+  \citeN{XXX}.
 
   An alternative, which provides us with a single type for states of automata,
   is to give every state node an identity, for example a natural number, and
@@ -2560,7 +2562,7 @@
   Myhill-Nerode Theorem. One direct proof using tagging-functions and
   another using partial derivatives. This part of our work is where
   our method using regular expressions shines, because we can perform
-  an induction on the structure of refular expressions. However, it is
+  an induction on the structure of regular expressions. However, it is
   also the direction where we had to spend most of the `conceptual'
   time, as our first proof based on tagging-functions is new for
   establishing the Myhill-Nerode Theorem. All standard proofs of this
@@ -2662,8 +2664,12 @@
   then regular expressions are easier to work with formally. 
   The code of
   our formalisation \cite{myhillnerodeafp11} can be found in the Archive of Formal Proofs at 
-  \mbox{\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}}.\smallskip
+  \mbox{\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}}.
   
+  Our future work will focus on formalising the regular expression matchers
+  developed by \citeN{Sulzmann12} which generate variable assignments for
+  regular expression submatching.\smallskip
+
   \noindent
   {\bf Acknowledgements:}
   We are grateful for the comments we received from Larry Paulson.  Tobias

--- a/Journal/document/root.bib	Thu Sep 12 10:34:11 2013 +0200
+++ b/Journal/document/root.bib	Thu Sep 12 17:20:48 2013 +0100
@@ -426,3 +426,10 @@
   year = 	"2002",
 }
 
+@InProceedings{Sulzmann12,
+  title =	"M.~Sulzmann and K.~Z.~M.~Lu",
+  author =	"XXX", 
+  booktitle =	"Proc. of XXX",
+  year = 	"2012",
+  pages =	"XXX"
+}

Binary file journal.pdf has changed