diff -r 199cf7ce1169 -r 3c504ca0ce95 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 07 03:33:32 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 03:37:02 2013 +0000
@@ -1371,10 +1371,13 @@
   we can strengthen this result slightly by observing that @{text m} is at most
   2 in the output tape. This observation allows one to construct a UTM that works
   entirely on the left-tape by composing it with a machine that drags the tape
-  two cells to the right. A corolary is that one-sided Turing machines (where the
-  tape only extends to the right) are as powerful as our two-sided Turing machines. 
+  two cells to the right. A corollary is that one-sided Turing machines (where the
+  tape only extends to the right) are computationally as powerful as our two-sided 
+  Turing machines. So our undecidability proof for the halting problem extends
+  also to one-sided Turing machines, which is needed for example in order to
+  formalise the undecidability of Wang's tiling problem \cite{Robinson71}.
 
-  While formalising the chapter about universal Turing machines in \cite{Boolos87}
+  While formalising the chapter about universal Turing machines in \cite{Boolos87},
   we noticed that they use their definition about what function Turing machines
   calculate. They write in Chapter 3 \cite[Page 32]{Boolos87}: