diff -r 47446f111550 -r 061b32d78471 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Sep 08 15:08:02 2011 +0000
+++ b/Journal/Paper.thy	Mon Sep 12 19:50:21 2011 +0000
@@ -427,7 +427,7 @@
   regular expressions. This theorem gives necessary and sufficient conditions
   for when a language is regular. As a corollary of this theorem we can easily
   establish the usual closure properties, including complementation, for
-  regular languages. We use the continuation lemma \cite{Rosenberg06}, 
+  regular languages. We use the Continuation Lemma \cite{Rosenberg06}, 
   which is also a corollary of the Myhill-Nerode Theorem, for establishing 
   the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip
   
@@ -2398,8 +2398,8 @@
   equational system is set up. We have the $\lambda$-term on our `initial
   state', while Brzozowski has it on the terminal states. This means we also
   need to reverse the direction of Arden's Lemma. We have not found anything
-  in the literature about our way of proving the first direction of the
-  Myhill-Nerode Theorem, but it appears to be folklore.
+  in the `pencil-and-paper-reasoning' literature about our way of proving the 
+  first direction of the Myhill-Nerode Theorem, but it appears to be folklore.
 
   We presented two proofs for the second direction of the Myhill-Nerode
   Theorem. One direct proof using tagging-functions and another using partial