--- a/Journal/Paper.thy	Mon Feb 20 11:02:50 2012 +0000
+++ b/Journal/Paper.thy	Wed Feb 22 13:25:49 2012 +0000
@@ -6,7 +6,7 @@
 declare [[show_question_marks = false]]
 
 consts
- REL :: "(string \<times> string) \<Rightarrow> bool"
+ REL :: "(string \<times> string) set"
  UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
 
 abbreviation
@@ -326,7 +326,8 @@
   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.}
+  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.}
 
   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
@@ -391,7 +392,8 @@
   completeness of automata, that is automata need to have total transition
   functions and at most one `sink' state from which there is no connection to
   a final state (Brzozowski mentions this side-condition in the context of
-  state complexity of automata \cite{Brzozowski10}). Such side-conditions mean
+  state complexity of automata \cite{Brzozowski10}, but it is also needed
+  in the usual construction of the complement automaton). Such side-conditions mean
   that if we define a regular language as one for which there exists \emph{a}
   finite automaton that recognises all its strings (see
   Definition~\ref{baddef}), then we need a lemma which ensures that another
@@ -609,7 +611,6 @@
   also with other functions.
 *}
 
-
 section {* The Myhill-Nerode Theorem, First Part *}
 
 text {*
@@ -2455,8 +2456,9 @@
   While our formalisation might appear large, it 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 magnitude of 18 months
-  for their formalisation. It is hard to gauge the size of a
+  that their four-member team would need something on the magnitude of 18 months
+  for their formalisation of the first eleven chapters of \cite{HopcroftUllman69}, 
+  which includes the Myhill-Nerode theorem. 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. We attribute
   this to our use of regular expressions, which meant we did not need to `fight'