diff -r bcef7669f55a -r c21aaf7723a0 Journal/Paper.thy --- 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