diff -r cf6e89b5f702 -r 904f9351ab94 Paper/Paper.thy
--- a/Paper/Paper.thy	Sat Jan 26 21:46:12 2013 +0000
+++ b/Paper/Paper.thy	Sun Jan 27 00:09:17 2013 +0000
@@ -182,8 +182,9 @@
 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
 our formalisation we follow mainly the proofs from the textbook
 \cite{Boolos87} and found that the description there is quite
-detailed. Some details are left out however: for example, it is only
-shown how the universal Turing machine is constructed for Turing
+detailed. Some details are left out however: for example, constructing
+the \emph{copy Turing program} is left as an excerise; also the 
+book only shows how the universal Turing machine is constructed for Turing
 machines computing unary functions. We had to figure out a way to
 generalise this result to $n$-ary functions. Similarly, when compiling
 recursive functions to abacus machines, the textbook again only shows
@@ -257,7 +258,7 @@
   r)"}, where @{term l} stands for the tape on the left-hand side of
   the head and @{term r} for the tape on the right-hand side.  We use
   the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
-  composed of @{term n} elements of @{term Bk}.  We also have the
+  composed of @{term n} elements of @{term Bk}s.  We also have the
   convention that the head, abbreviated @{term hd}, of the right-list
   is the cell on which the head of the Turing machine currently
   scannes. This can be pictured as follows:
@@ -552,9 +553,9 @@
   \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
   \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
   \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
-  \node [anchor=base] at (2.2,-0.5) {\small@{term "tcopy_init"}};
-  \node [anchor=base] at (5.6,-0.5) {\small@{term "tcopy_loop"}};
-  \node [anchor=base] at (10.5,-0.5) {\small@{term "tcopy_end"}};
+  \node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_init"}}^{}$};
+  \node [anchor=base] at (5.6,-0.6) {\small$\overbrace{@{term "tcopy_loop"}}^{}$};
+  \node [anchor=base] at (10.5,-0.6) {\small$\overbrace{@{term "tcopy_end"}}^{}$};
 
 
   \begin{scope}[shift={(0.5,0)}]
@@ -628,10 +629,10 @@
   \end{tikzpicture}\\[-8mm]\mbox{} 
   \end{center}
   \caption{The components of the \emph{copy Turing machine} (above). If started 
-  with the tape @{term "([], <[(3::nat)]>)"} the first machine adds @{term "[Bk, Oc]"} at 
+  with the tape @{term "([], <[(2::nat)]>)"} the first machine adds @{term "[Bk, Oc]"} at 
   the end of the right tape; the second then ``moves'' all @{term Oc}s except the 
   first from the beginning of the tape to the end; the third ``refills'' the original 
-  block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(3::nat, 3::nat)]>)"}.}
+  block of @{term "Oc"}s. The result is the tape @{term "([Bk], <[(2::nat, 2::nat)]>)"}.}
   \label{copy}
   \end{figure}