--- a/Paper/Paper.thy	Tue Feb 19 04:56:33 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 19 05:11:33 2013 +0000
@@ -1398,7 +1398,9 @@
   Turing machines, an unexpected outcome of our work is that we
   identified an inconsistency in their use of a definition. This is
   unexpected since \cite{Boolos87} is a classic textbook which has
-  undergone several editions (we used the fifth edition). The central
+  undergone several editions (we used the fifth edition; the material 
+  containing the inconsistency was introduced in the fourth edition
+  \cite{BoolosFourth}). The central
   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

--- a/Paper/document/root.bib	Tue Feb 19 04:56:33 2013 +0000
+++ b/Paper/document/root.bib	Tue Feb 19 05:11:33 2013 +0000
@@ -74,6 +74,14 @@
   year      = {2007}
 }
 
+@book{BoolosFourth,
+  author    = {G.~Boolos and J.~P.~Burgess and R.~C.~Jeffrey},
+  title     = {{C}omputability and {L}ogic (4th~ed.)},
+  publisher = {Cambridge University Press},
+  year      = {2002}
+}
+
+
 @inproceedings{WuZhangUrban11,
   author    = {C.~Wu and X.~Zhang and C.~Urban},
   title     = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions

--- a/ROOT	Tue Feb 19 04:56:33 2013 +0000
+++ b/ROOT	Tue Feb 19 05:11:33 2013 +0000
@@ -10,3 +10,7 @@
     "thys/Recursive"
     "thys/UF"
     "thys/UTM"
+
+session ITP = UTM +
+  theories
+    "Paper/Paper"
\ No newline at end of file

Binary file paper.pdf has changed