diff -r 7971da47e8c4 -r ae3d568b887b Paper.thy
--- a/Paper.thy	Thu Jan 10 07:20:28 2013 +0000
+++ b/Paper.thy	Thu Jan 10 07:33:51 2013 +0000
@@ -117,7 +117,7 @@
 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 Section~\ref{Wang}. The
+example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The
 standard proof of this property uses the notion of \emph{universal
 Turing machines}.
 
@@ -157,20 +157,20 @@
 \noindent
 In this paper we follow the approach by Boolos et al \cite{Boolos87},
 which goes back to Post \cite{Post36}, where all Turing machines
-operate on tapes that contain only \emph{blank} or \emph{filled} cells
+operate on tapes that contain only \emph{blank} or \emph{occupied} cells
 (represented by @{term Bk} and @{term Oc}, respectively, in our
 formalisation). Traditionally the content of a cell can be any
 character from a finite alphabet. Although computationally equivalent,
 the more restrictive notion of Turing machines in \cite{Boolos87} makes
 the reasoning more uniform. In addition some proofs \emph{about} Turing
-machines will be simpler.  The reason is that one often need to encode
-Turing machines---if the Turing machines are simpler, then the coding
-functions are simpler. Unfortunately, the restrictiveness also makes
+machines will be simpler.  The reason is that one often needs to encode
+Turing machines---consequently if the Turing machines are simpler, then the coding
+functions are simpler too. Unfortunately, the restrictiveness also makes
 it harder to design programs for these Turing machines. Therefore in order
 to construct a \emph{universal Turing machine} we follow the proof in
 \cite{Boolos87} by relating abacus machines to Turing machines and in
 turn recursive functions to abacus machines. The universal Turing
-machine can then be constructed as recursive function.
+machine can then be constructed as a recursive function.
 
 \smallskip
 \noindent
@@ -180,16 +180,15 @@
 
 section {* Turing Machines *}
 
-text {*
-  \noindent
-  Turing machines can be thought of as having read-write-unit
+text {* \noindent
+  Turing machines can be thought of as having a read-write-unit
   ``gliding'' over a potentially infinite tape. Boolos et
   al~\cite{Boolos87} only consider tapes with cells being either blank
-  or occupied, which we represent with a datatype having two
-  constructors, namely @{text Bk} and @{text Oc}.  One easy way to
+  or occupied, which we represent by a datatype having two
+  constructors, namely @{text Bk} and @{text Oc}.  One way to
   represent such tapes is to use a pair of lists, written @{term "(l,
-  r)"}, where @{term l} stands for the tape on the left of the
-  read-write-unit and @{term r} for the tape on the right. We have the
+  r)"}, where @{term l} stands for the tape on the left-hand side of the
+  read-write-unit and @{term r} for the tape on the right-hand side. We have the
   convention that the head, written @{term hd}, of the right-list is
   the cell on which the read-write-unit currently operates. This can
   be pictured as follows:
@@ -238,10 +237,10 @@
   \end{center}
 
   \noindent
-  By using the @{term Nop} operation, we slightly deviate
-  from the presentation in \cite{Boolos87}; however its use
+  We slightly deviate
+  from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
   will become important when we formalise universal Turing 
-  machines. Given a tape and an action, we can define the
+  machines later. Given a tape and an action, we can define the
   following updating function:
 
   \begin{center}
@@ -249,9 +248,9 @@
   @{thm (lhs) new_tape_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(1)}\\
   @{thm (lhs) new_tape_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(2)}\\
   @{thm (lhs) new_tape_def2(3)} & @{text "\<equiv>"} & \\
-  \multicolumn{3}{p{3cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\
+  \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\
   @{thm (lhs) new_tape_def2(4)} & @{text "\<equiv>"} & \\
-  \multicolumn{3}{p{2cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\
+  \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\
   @{thm (lhs) new_tape_def2(5)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(5)}\\
   \end{tabular}
   \end{center}