diff -r 38d8e0e37b7d -r 0f52b971cc03 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 07 03:01:51 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 03:14:58 2013 +0000
@@ -1329,37 +1329,48 @@
   with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
   with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
 
-  Having 
-
-  we can prove that if 
+  Having recursive functions under our belt, we can construct an universal
+  function and consider the translated (universal) Turing machine @{term UTM}. 
+  Suppose
+  a Turing program is well-formed and @{term p} when started with the standard 
+  tape containing the arguments @{term arg}, produces a standard tape
+  with ``output'' @{term n}. This assumption can be written as the
+  Hoare-triple
 
   \begin{center}
   @{thm (prem 3) UTM_halt_lemma2}
   \end{center}
-  then 
+  
+  \noindent
+  where we assume the @{term args} are non-empty, then the universal Turing
+  machine @{term UTM} started with the code of @{term p} and the arguments
+  @{term args} calculates the same result:
 
   \begin{center}
   @{thm (concl) UTM_halt_lemma2} 
   \end{center}
 
-  under the assumption that @{text p}
-  is well-formed and the arguments are not empty.
-
+  \noindent
+  Similarly, if a Turing program @{term p} started with the 
+  standard tape containing @{text args} loops, which is represented
+  by the Hoare-pair
 
   \begin{center}
   @{thm (prem 2) UTM_unhalt_lemma2}
   \end{center}
-  then 
+
+  \noindent
+  then the universal Turing machine started with the code of @{term p} and the arguments
+  @{term args} will also loop
 
   \begin{center}
   @{thm (concl) UTM_unhalt_lemma2} 
   \end{center}
 
-
-  and the also the definition of the
-  universal function (we refer the reader to our formalisation).
-
-  \cite[Page 32]{Boolos87}
+  \noindent
+  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}:
 
   \begin{quote}\it
   ``If the function that is to be computed assigns no value to the arguments that 
@@ -1367,6 +1378,10 @@
   or will halt in some nonstandard configuration\ldots''
   \end{quote}
   
+  \noindent
+  Interestingly, they do not implement this definition when considering 
+  their universal Turing machine.
+
   This means that if you encode the plus function but only give one argument,
   then the TM will either loop {\bf or} stop with a non-standard tape