diff -r 2c0d79801e36 -r a4601143db90 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 07 04:28:00 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 04:53:29 2013 +0000
@@ -1330,8 +1330,22 @@
   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 recursive functions under our belt, we can construct an universal
-  function and consider its translated (universal) Turing machine, written @{term UTM}. 
+  Having recursive functions under our belt, we can construct a universal
+  function, written @{text UF}. This universal function acts like an interpreter for Turing machines.
+  It takes two arguments: one is the code of the Turing machine to be interpreted and the 
+  other is the ``packed version'' of the arguments of the Turing machine. 
+  We can then consider how this universal function is translated to a 
+  Turing machine and from this construct the universal Turing machine, 
+  written @{term UTM}. @{text UTM} is defined as 
+  the composition of the Turing machine that packages the arguments and
+  the translated recursive 
+  function @{text UF}:
+
+  \begin{center}
+  @{text "UTM \<equiv> arg_coding \<oplus> (translate UF)"}
+  \end{center}
+
+  \noindent
   Suppose
   a Turing program @{term p} is well-formed and  when started with the standard 
   tape containing the arguments @{term args}, will produce a standard tape
@@ -1343,9 +1357,9 @@
   \end{center}
   
   \noindent
-  where we assume the @{term args} stand for a non-empty list. Then the universal Turing
+  where we require that the @{term args} stand for a non-empty list. Then the universal Turing
   machine @{term UTM} started with the code of @{term p} and the arguments
-  @{term args} calculates the same result, namely
+  @{term args}, calculates the same result, namely
 
   \begin{center}
   @{thm (concl) UTM_halt_lemma2} 
@@ -1502,11 +1516,11 @@
   decidability of a predicate @{text P}, say, as the formula @{term "P
   \<or> \<not>P"}. For reasoning about computability we need to formalise a
   concrete model of computations. We could have followed Norrish
-  \cite{Norrish11} using the $\lambda$-calculus as the starting point,
+  \cite{Norrish11} using the $\lambda$-calculus as the starting point for computability theory,
   but then we would have to reimplement his infrastructure for
   reducing $\lambda$-terms on the ML-level. We would still need to
   connect his work to Turing machines for proofs that make essential use of them
-  (for example the proof of Wang's tiling problem \cite{Robinson71}).
+  (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}).
 
   We therefore have formalised Turing machines and the main
   computability results from Chapters 3 to 8 in the textbook by Boolos