--- a/Paper/Paper.thy	Thu Feb 07 05:23:53 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 05:32:00 2013 +0000
@@ -327,9 +327,12 @@
 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,
+machines. This works essentially like a small, verified compiler 
+from recursive functions to Turing machine programs.
+When formalising the universal Turing machine,
 we stumbled upon an inconsistent use of the definition of
-what function a Turing machine calculates. 
+what partial 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
@@ -1529,17 +1532,17 @@
   connect his work to Turing machines for proofs that make essential use of them
   (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).
 
-  We therefore have formalised Turing machines and the main
+  We therefore have formalised Turing machines in the first place and the main
   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 Bolos et al's 
+  \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
   tape. Whereas in Chapter 8 about the universal Turing machine, the
   Turing machines will \emph{not} halt unless the tape is in standard
-  form. If the title had not already been taken \cite{Nipkow98}, we could
+  form. If the title had not already been taken in \cite{Nipkow98}, we could
   have titled our paper ``Boolos et al are (almost)
   Right''. We have not attempted to formalise everything precisely as
   Boolos et al present it, but use definitions that make our

Binary file paper.pdf has changed