# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360215120 0
# Node ID 6a584d61820f17b03429f28f2a2f478cf32f96cb
# Parent  fe0e6733b9e4074b7134205efdda3c12078a1bd8
updated paper

diff -r fe0e6733b9e4 -r 6a584d61820f Paper/Paper.thy
--- 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
diff -r fe0e6733b9e4 -r 6a584d61820f paper.pdf
Binary file paper.pdf has changed