--- a/Journal/Paper.thy	Thu Jul 11 12:07:11 2013 +0100
+++ b/Journal/Paper.thy	Thu Jul 11 16:46:05 2013 +0100
@@ -1732,7 +1732,7 @@
 
   \begin{rmk}
   While our proof using tagging functions might seem like a rabbit pulled 
-  out of a hat, the intuition behind can be somewhat rationalised taking the 
+  out of a hat, the intuition behind can be somewhat rationalised by taking the 
   view that the equivalence classes @{term "UNIV // \<approx>(lang r)"} stand for the 
   states of the minimal automaton for the language @{term "lang r"}. The theorem 
   amounts to showing that this minimal automaton has finitely many states. 
@@ -2646,7 +2646,7 @@
   regular language theory and Kleene algebras in Coq. While he is
   mainly interested in implementing decision procedures for Kleene
   algebras, his library includes a proof of the Myhill-Nerode
-  theorem. He reckons that our ``development is more concise'' than
+  theorem. He reckons that our Myhill-Nerode ``development is more concise'' than
   his one based on matrices \cite[Page 67]{Braibant12}.  He writes
   that there is no conceptual problems with formally reasoning about
   matrices for automata, but notes ``intrinsic difficult[ies]'' when