--- a/Paper.thy	Sun Jan 06 23:50:24 2013 +0000
+++ b/Paper.thy	Tue Jan 08 01:21:02 2013 +0000
@@ -60,33 +60,33 @@
 theorem provers, like Isabelle/HOL, are at their best when the
 data-structures at hand are ``structurally'' defined, like lists,
 natural numbers, regular expressions, etc. Such data-structures come
-convenient reasoning infrastructures (for
+with convenient reasoning infrastructures (for
 example induction principles, recursion combinators and so on).  But
 this is \emph{not} the case with Turing machines (and also not with
 register machines): underlying their definition is a set of states
 together with a transition function, both of which are not
 structurally defined.  This means we have to implement our own
 reasoning infrastructure in order to prove properties about them. This
-leads to annoyingly lengthy and fiddly formalisations.  We noticed
-first the difference between both structural and non-structural
+leads to annoyingly fiddly formalisations.  We noticed
+first the difference between both, structural and non-structural,
 ``worlds'' when formalising the Myhill-Nerode theorem, where regular
 expressions fared much better than automata \cite{WuZhangUrban11}.
 However, with Turing machines there seems to be no alternative if one
 wants to formalise the great many proofs from the literature that use them.
 We will analyse one example---undecidability of Wang tilings---in 
-detail in Section~\ref{Wang}. The standard proof of this property uses 
+Section~\ref{Wang}. The standard proof of this property uses 
 the notion of \emph{universal Turing machines}.
 
 We are not the first who formalised Turing machines in a theorem
 prover: we are aware of the preliminary work by Asperti and Ricciotti
 \cite{AspertiRicciotti12}. They describe a complete formalisation of Turing
-machines in the Matita theorem prover, including an universal Turing
+machines in the Matita theorem prover, including a universal Turing
 machine. They report 
 that the informal proofs from which they started are not 
 ``sufficiently accurate to be directly used as a guideline for 
 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation 
 we followed the proofs from the textbook \cite{Boolos87} and found that the description
-is quite detailed. Some details are left out however: for 
+there is quite detailed. Some details are left out however: for 
 example, it is only shown how the universal
 Turing machine is constructed for Turing machines computing unary 
 functions. We had to figure out a way to generalize this result to
@@ -99,7 +99,7 @@
 The main difference between our formalisation and the one by Asperti and
 Ricciotti  is that their universal Turing 
 machine uses a different alphabet than the machines it simulates. They
-write \cite[Page XXX]{AspertiRicciotti12}:
+write \cite[Page 23]{AspertiRicciotti12}:
 
 \begin{quote}\it
 ``In particular, the fact that the universal machine operates with a
@@ -112,7 +112,7 @@
 where Turing machines (and our
 universal Turing machine) operates on tapes that contain only blank
 or filled cells (respectively represented by 0 and 1---or in our 
-formalisation by @{term Bk} or @{term Oc}).
+formalisation by @{term Bk} and @{term Oc}).