--- a/Paper/Paper.thy	Tue Feb 05 10:11:38 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 10:12:56 2013 +0000
@@ -1180,7 +1180,7 @@
   Turing machine programs. Registers and their content are represented by
   standard tapes. Because of the jumps in abacus programs, it
   seems difficult to build a Turing machine programs out of components 
-  using our @{text "\<oplus>"}-operation.
+  using our @{text "\<oplus>"}-operation shown in the previous section.
   To overcome this difficulty, we calculate a \emph{layout} as follows
 
   \begin{center}