--- a/Paper.thy	Thu Jan 10 13:03:25 2013 +0000
+++ b/Paper.thy	Thu Jan 10 13:13:27 2013 +0000
@@ -315,7 +315,15 @@
 
   An \emph{instruction} @{term i} of a Turing machine is a pair consisting of a
   natural number (the next state) and an action. A \emph{program} @{term p} of a Turing
-  machine is then a list of such pairs. Given a program @{term p}, a state
+  machine is then a list of such pairs. We have organised our programs
+  such that 
+
+  \begin{center}
+  XXX
+  \end{center}
+
+  \noindent
+  Given a program @{term p}, a state
   and the cell being read by the read-write unit, we need to fetch
   the corresponding instruction from the program. For this we define 
   the function @{term fetch}
@@ -425,6 +433,9 @@
   have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which
   sets the value of $R$ to $n$, and if $R$ was not yet in $m$
   it pads it approriately with 0s.
+
+
+  Abacus machine halts when it jumps out of range.
 *}