--- a/Paper/Paper.thy	Sat Feb 19 20:15:59 2011 +0000
+++ b/Paper/Paper.thy	Sat Feb 19 21:49:11 2011 +0000
@@ -36,8 +36,11 @@
   append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
   uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
   tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
-  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100)
-
+  tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
+  tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
+  tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
+  tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
+  tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
 lemma meta_eq_app:
   shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
   by auto
@@ -265,7 +268,7 @@
   string; this property states that if @{term "[] \<notin> A"} then the lengths of
   the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}.  We omit
   the proofs for these properties, but invite the reader to consult our
-  formalisation.\footnote{Available at ???}
+  formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/regexp/}}
 
   The notation in Isabelle/HOL for the quotient of a language @{text A} according to an 
   equivalence relation @{term REL} is @{term "A // REL"}. We will write 
@@ -999,9 +1002,24 @@
   \end{proof}
 
 
-  @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]}
- 
-  @{thm tag_str_STAR_def[where ?L1.0="A"]}
+  \noindent
+  The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
+  they are slightly more complicated. 
+
+
+  \begin{proof}[@{const SEQ}-Case]
+
+  \begin{center}
+  @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+  \end{center}
+  \end{proof}
+
+  \begin{proof}[@{const STAR}-Case]
+
+  \begin{center}
+  @{thm tag_str_STAR_def[where ?L1.0="A", THEN meta_eq_app]}
+  \end{center}
+  \end{proof}
 *}
 
 
@@ -1046,8 +1064,9 @@
   established, we refer the reader to Owens and Slind \cite{OwensSlind08}.
 
 
-  Our formalisation consists of ??? lines of Isabelle/Isar code for the first
-  direction and ??? for the second. While this might be seen as too large to
+  Our formalisation consists of 790 lines of Isabelle/Isar code for the first
+  direction and 475 for the second, plus standard material about regular languages. 
+  While this might be seen as too large to
   count as a concise proof pearl, this 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. 
@@ -1060,10 +1079,10 @@
   was not the bottleneck. 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. The code of
-  ours can be found under
+  ours can be found in the Mercurial Repository at
 
   \begin{center}
-  ???
+  \url{http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/regexp/}
   \end{center}
 
 
@@ -1095,7 +1114,9 @@
   is also where our method shines, because we can completely side-step the
   standard argument \cite{Kozen97} where automata need to be composed, which
   as stated in the Introduction is not so convenient to formalise in a 
-  HOL-based theorem prover.
+  HOL-based theorem prover. However, it is also the direction where we had to 
+  spend most of the `conceptual' time, as our proof-argument based on tagging functions
+  is new for establishing the Myhill-Nerode theorem.
 
 *}