# HG changeset patch
# User urbanc
# Date 1298206355 0
# Node ID 9dd70b10d90c6a86dab21163b470d84920f10555
# Parent  6d2693c78c37584d6b26e1b6d847225f1b2dc2e2
minor

diff -r 6d2693c78c37 -r 9dd70b10d90c Paper/Paper.thy
--- 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