--- a/Paper/Paper.thy	Thu Feb 07 04:53:29 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 04:56:01 2013 +0000
@@ -1392,14 +1392,15 @@
   %also to one-sided Turing machines, which is needed for example in order to
   %formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
 
-  While formalising the chapter in  \cite{Boolos87} about universal Turing machines, an
-  unexpected outcome is that we identified an inconsistency in
-  their use of a definition. It is unexpected since it is a classic textbook which has
-  undergone several editions. The main idea is that every Turing machine started with
-  a standard tape computes a
-  partial arithmetic function.  The inconsitency is when they define
-  when this function should \emph{not} return a result. They write in Chapter
-  3 \cite[Page 32]{Boolos87}:
+  While formalising the chapter in \cite{Boolos87} about universal
+  Turing machines, an unexpected outcome of our work is that we
+  identified an inconsistency in their use of a definition. This is
+  unexpected since \cite{Boolos87} is a classic textbook which has
+  undergone several editions (we used the fifth edition). The central
+  idea about Turing machines is that when started with standard tapes
+  they compute a partial arithmetic function.  The inconsitency is
+  when they define when this function should \emph{not} return a
+  result. They write in Chapter 3 \cite[Page 32]{Boolos87}:
 
   \begin{quote}\it
   ``If the function that is to be computed assigns no value to the arguments that