--- a/Paper/Paper.thy	Wed Feb 06 14:14:35 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 00:46:04 2013 +0000
@@ -229,7 +229,7 @@
 of register machines) and recursive functions. To see the difficulties
 involved with this work, one has to understand that Turing machine
 programs can be completely \emph{unstructured}, behaving similar to
-Basic programs containing the infamous gotos \cite{Dijkstra68}. This
+Basic programs containing the infamous goto \cite{Dijkstra68}. This
 precludes in the general case a compositional Hoare-style reasoning
 about Turing programs.  We provide such Hoare-rules for when it
 \emph{is} possible to reason in a compositional manner (which is
@@ -318,22 +318,25 @@
 
 \smallskip
 \noindent
-{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the
-description of Boolos et al \cite{Boolos87} where tapes only have blank or
-occupied cells. We mechanise the undecidability of the halting problem and
-prove the correctness of concrete Turing machines that are needed
-in this proof; such correctness proofs are left out in the informal literature.  
-For reasoning about Turing machine programs we derive Hoare-rules.
-We also construct the universal Turing machine from \cite{Boolos87} by
-translating recursive functions to abacus machines and abacus machines to
-Turing machines. Since we have set up in Isabelle/HOL a very general computability
-model and undecidability result, we are able to formalise other
-results: we describe a proof of the computational equivalence
-of single-sided Turing machines, which is not given in \cite{Boolos87},
-but needed for example for formalising the undecidability proof of 
-Wang's tiling problem \cite{Robinson71}.
-%We are not aware of any other
-%formalisation of a substantial undecidability problem.
+{\bf Contributions:} We formalised in Isabelle/HOL Turing machines
+following the description of Boolos et al \cite{Boolos87} where tapes
+only have blank or occupied cells. We mechanise the undecidability of
+the halting problem and prove the correctness of concrete Turing
+machines that are needed in this proof; such correctness proofs are
+left out in the informal literature.  For reasoning about Turing
+machine programs we derive Hoare-rules.  We also construct the
+universal Turing machine from \cite{Boolos87} by translating recursive
+functions to abacus machines and abacus machines to Turing
+machines. When formalising the universal Turing machine,
+we stumbled upon an inconsistence use of the definition of
+what function a Turing machine calculates. Since we have set up in
+Isabelle/HOL a very general computability model and undecidability
+result, we are able to formalise other results: we describe a proof of
+the computational equivalence of single-sided Turing machines, which
+is not given in \cite{Boolos87}, but needed for example for
+formalising the undecidability proof of Wang's tiling problem
+\cite{Robinson71}.  %We are not aware of any other %formalisation of a
+substantial undecidability problem.
 *}
 
 section {* Turing Machines *}
@@ -747,7 +750,8 @@
   \end{equation}
   %
   \noindent
-  A \emph{standard tape} is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l} 
+  A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k}, 
+  @{text l} 
   and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the 
   leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0} 
   is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
@@ -977,7 +981,7 @@
 
   \noindent
   This invariant depends on @{term n} representing the number of
-  @{term Oc}s@{text "+1"} (or encoded number) on the tape. It is not hard (26
+  @{term Oc}s on the tape. It is not hard (26
   lines of automated proof script) to show that for @{term "n >
   (0::nat)"} this invariant is preserved under the computation rules
   @{term step} and @{term steps}. This gives us partial correctness