diff -r cf253ae0c4d6 -r a63c3f8d7234 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 07 06:10:11 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 06:39:06 2013 +0000
@@ -1214,8 +1214,8 @@
   \noindent
   This gives us a list of natural numbers specifying how many states
   are needed to translate each abacus instruction. This information
-  is needed in order to calculate the state where the Turing program
-  code of one abacus instruction ends and the next starts.
+  is needed in order to calculate the state where the Turing machine program
+  of one abacus instruction ends and the next starts.
   The @{text Goto}
   instruction is easiest to translate requiring only one state, namely
   the Turing machine program:
@@ -1260,7 +1260,7 @@
   program is assumed to calculate a value stored in the last
   register (the one with the highest register). That means we have to append a Turing machine that
   ``mops up'' the tape (cleaning all @{text Oc}s) except for the
-  @{term Oc}s of the last number represented on the tape. This needs
+  @{term Oc}s of the last register represented on the tape. This needs
   a Turing machine program with @{text "2 * R + 12"} states, assuming @{text R}
   is the number of registers to be ``cleaned''.
 
@@ -1536,7 +1536,7 @@
   computability results from Chapters 3 to 8 in the textbook by Boolos
   et al \cite{Boolos87}.  For this we did not need to implement
   anything on the ML-level of Isabelle/HOL. While formalising the six chapters
-  \cite{Boolos87} we have found an inconsistency in Boolos et al's 
+  of \cite{Boolos87} we have found an inconsistency in Boolos et al's 
   definitions of what function a Turing machine calculates. In
   Chapter 3 they use a definition that states a function is undefined
   if the Turing machine loops \emph{or} halts with a non-standard