--- a/Paper/Paper.thy	Sun Feb 20 12:51:04 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 12:52:35 2011 +0000
@@ -1151,7 +1151,8 @@
   By the assumption about @{term "tag_str_SEQ A B"} we have
   @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
   relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude aslo in this case
-  with @{term "y @ z \<in> A ;; B"}. That completes the @{const SEQ}-case.\qed 
+  with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case
+  by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed 
   \end{proof}
   
   \noindent