--- a/Paper/Paper.thy	Sun Jan 27 00:09:17 2013 +0000
+++ b/Paper/Paper.thy	Sun Jan 27 14:57:54 2013 +0000
@@ -183,8 +183,8 @@
 our formalisation we follow mainly the proofs from the textbook
 \cite{Boolos87} and found that the description there is quite
 detailed. Some details are left out however: for example, constructing
-the \emph{copy Turing program} is left as an excerise; also the 
-book only shows how the universal Turing machine is constructed for Turing
+the \emph{copy Turing program} is left as an excerise to the reader; also 
+\cite{Boolos87} only shows how the universal Turing machine is constructed for Turing
 machines computing unary functions. We had to figure out a way to
 generalise this result to $n$-ary functions. Similarly, when compiling
 recursive functions to abacus machines, the textbook again only shows
@@ -259,7 +259,7 @@
   the head and @{term r} for the tape on the right-hand side.  We use
   the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
   composed of @{term n} elements of @{term Bk}s.  We also have the
-  convention that the head, abbreviated @{term hd}, of the right-list
+  convention that the head, abbreviated @{term hd}, of the right list
   is the cell on which the head of the Turing machine currently
   scannes. This can be pictured as follows:
   %
@@ -329,20 +329,20 @@
   \end{center}
 
   \noindent
-  The first two clauses replace the head of the right-list
+  The first two clauses replace the head of the right list
   with a new @{term Bk} or @{term Oc}, respectively. To see that
   these two clauses make sense in case where @{text r} is the empty
   list, one has to know that the tail function, @{term tl}, is defined
   such that @{term "tl [] == []"} holds. The third clause 
   implements the move of the head one step to the left: we need
   to test if the left-list @{term l} is empty; if yes, then we just prepend a 
-  blank cell to the right-list; otherwise we have to remove the
-  head from the left-list and prepend it to the right-list. Similarly
+  blank cell to the right list; otherwise we have to remove the
+  head from the left-list and prepend it to the right list. Similarly
   in the fourth clause for a right move action. The @{term Nop} operation
   leaves the the tape unchanged.
 
   %Note that our treatment of the tape is rather ``unsymmetric''---we
-  %have the convention that the head of the right-list is where the
+  %have the convention that the head of the right list is where the
   %head is currently positioned. Asperti and Ricciotti
   %\cite{AspertiRicciotti12} also considered such a representation, but
   %dismiss it as it complicates their definition for \emph{tape
@@ -629,10 +629,10 @@
   \end{tikzpicture}\\[-8mm]\mbox{} 
   \end{center}
   \caption{The components of the \emph{copy Turing machine} (above). If started 
-  with the tape @{term "([], <[(2::nat)]>)"} the first machine adds @{term "[Bk, Oc]"} at 
+  with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at 
   the end of the right tape; the second then ``moves'' all @{term Oc}s except the 
   first from the beginning of the tape to the end; the third ``refills'' the original 
-  block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(2::nat, 2::nat)]>)"}.}
+  block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}
   \label{copy}
   \end{figure}