--- a/Journal/Paper.thy	Wed Sep 14 13:39:03 2011 +0000
+++ b/Journal/Paper.thy	Wed Sep 14 15:56:03 2011 +0000
@@ -2302,7 +2302,7 @@
   That means we have to show that \mbox{@{text "\<forall>z. a\<^sup>i @ z \<in> A = a\<^sup>j @ z \<in> A"}} leads to 
   a contradiction. Let us take @{text "b\<^sup>i"} for @{text "z"}. Then we know @{text "a\<^sup>i @ b\<^sup>i \<in> A"}.
   But since @{term "i \<noteq> j"}, @{text "a\<^sup>j @ b\<^sup>i \<notin> A"}. Therefore  @{text "a\<^sup>i"} and @{text "a\<^sup>j"}
-  cannot be Myhill-Nerode related by @{text "A"} and we are done.
+  cannot be Myhill-Nerode related by @{text "A"}, and we are done.
   \end{proof}
 
   \noindent