--- a/Paper/Paper.thy	Tue Feb 19 05:11:33 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 19 13:36:35 2013 +0000
@@ -1196,7 +1196,7 @@
   The main point of abacus programs is to be able to translate them to 
   Turing machine programs. Registers and their content are represented by
   standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it
-  is impossible to build a Turing machine programs out of components 
+  is impossible to build Turing machine programs out of components 
   using our @{text "\<oplus>"}-operation shown in the previous section.
   To overcome this difficulty, we calculate a \emph{layout} of an
   abacus program as follows
@@ -1250,7 +1250,7 @@
   with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the 
   translated Turing machine needs to first check whether the content of the
   corresponding register is @{text 0}. For this we have a Turing machine program
-  with @{text 16} states (again details are omitted). 
+  with @{text 16} states (again the details are omitted). 
 
   Finally, having a Turing machine for each abacus instruction we need
   to ``stitch'' the Turing machines together into one so that each
@@ -1404,7 +1404,7 @@
   idea about Turing machines is that when started with standard tapes
   they compute a partial arithmetic function.  The inconsitency arises
   when they define the case when this function should \emph{not} return a
-  result. They write in Chapter 3, Page 32:
+  result. Boolos at al write in Chapter 3, Page 32:
 
   \begin{quote}\it
   ``If the function that is to be computed assigns no value to the arguments that 
@@ -1571,7 +1571,7 @@
   recursive functions 5000 loc and the universal Turing machine 10000 loc).
   
   Our work is also very much inspired by the formalisation of Turing
-  machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the
+  machines of Asperti and Ricciotti \cite{AspertiRicciotti12} in the
   Matita theorem prover. It turns out that their notion of
   realisability and our Hoare-triples are very similar, however we
   differ in some basic definitions for Turing machines. Asperti and

--- a/ROOT	Tue Feb 19 05:11:33 2013 +0000
+++ b/ROOT	Tue Feb 19 13:36:35 2013 +0000
@@ -12,5 +12,6 @@
     "thys/UTM"
 
 session ITP = UTM +
+  options [document = pdf, document_output = "."]
   theories
     "Paper/Paper"
\ No newline at end of file

Binary file paper.pdf has changed