--- a/Journal/Paper.thy	Sat Sep 14 14:08:19 2013 +0100
+++ b/Journal/Paper.thy	Tue Sep 17 11:21:58 2013 +0100
@@ -344,7 +344,7 @@
   2005.} Systems such as Coq permit quantification over types and thus can
   state such a definition.  This has been recently exploited in an
   elegant and short formalisation of the Myhill-Nerode theorem in Coq by
-  \citeN{Smolka13}, but as said this is not avaible to us working in Isabelle/HOL.
+  \citeN{Smolka13}, but as said this is not available to us working in Isabelle/HOL.
 
   An alternative, which provides us with a single type for states of automata,
   is to give every state node an identity, for example a natural number, and
@@ -1741,8 +1741,8 @@
   \end{proof}
 
   \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 by taking the 
+  While our proof using tagging functions might seem like a `rabbit pulled 
+  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. 
@@ -1968,7 +1968,7 @@
   but the one modulo @{text "ACI"}.  In principle, this can be done formally, 
   but it is very painful in a theorem prover---since there is no
   direct characterisation of the set of dissimilar derivatives. Therefore
-  \citeN{CoquandSiles12} who follow through this idea had to `stand on their  heads' and
+  \citeN{CoquandSiles12} who follow through this idea had to spend extra effort and
   first formalise the quite intricate notion of \emph{inductively finite sets} in 
   order to formalise this property.
 
@@ -2315,7 +2315,7 @@
   \noindent
   Our proof follows the one given by \citeN[Pages 92--95]{Shallit08}, except that we use
   Higman's Lemma, which is already proved in the Isabelle/HOL library by
-  Sternagel.
+  \citeN{Sternagel13}.
   Higman's Lemma allows us to infer that every language @{text A} of antichains, satisfying
   %
   \begin{equation}\label{higman}