--- a/Paper/Paper.thy	Mon Feb 04 01:17:09 2013 +0000
+++ b/Paper/Paper.thy	Mon Feb 04 01:47:26 2013 +0000
@@ -1130,9 +1130,9 @@
   for making it less laborious to write Turing machine
   programs. Abacus machines operate over a set of registers $R_0$,
   $R_1$, \ldots{} each being able to hold an arbitrary large natural
-  number.  We use natural numbers to refer to registers, but also to
-  refer to \emph{statements} of abacus programs. Statements are given
-  by the datatype
+  number.  We use natural numbers to refer to registers; we also use a natural number
+  to represent a program counter. An abacus 
+  program is a list of \emph{statements} defined by the datatype:
 
   \begin{center}
   \begin{tabular}{rcl@ {\hspace{10mm}}l}
@@ -1145,28 +1145,37 @@
   \end{center}
 
   \noindent
-  A \emph{program} of an abacus machine is a list of such
-  statements. For example the program clearing the register
-  $R$ (setting it to @{term "(0::nat)"}) can be defined as follows:
+  For example the program clearing the register $R$ (that is setting
+  it to @{term "(0::nat)"}) can be defined as follows:
 
   \begin{center}
   @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
   \end{center}
 
   \noindent
-  The second opcode @{term "Goto 0"} in this program means we 
-  jump back to the first statement, namely @{text "Dec R o"}.
-  The \emph{memory} $m$ of an abacus machine holding the values
-  of the registers is represented as a list of natural numbers.
-  We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
-  which looks up the content of register $R$; if $R$
-  is not in this list, then we return 0. Similarly we
-  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.
+  Running such a program means we start with the first instruction
+  then execute statements one after the other, unless there is a jump.  For
+  example the second statement the jump @{term "Goto 0"} in @{term clear} means
+  we jump back to the first statement closing the loop.  Like with our
+  Turing machines, we fetch statements from an abacus program such
+  that a jump out of ``range'' behaves like a @{term "Nop"}-action. In
+  this way it is easy to define a function @{term steps} that
+  executes @{term n} statements of an abacus program.
+  
 
 
-  Abacus machine halts when it jumps out of range.
+  %Running an abacus program means to start 
+  %A \emph{program} of an abacus machine is a list of such
+  %statements. 
+  %The \emph{memory} $m$ of an abacus machine holding the values
+  %of the registers is represented as a list of natural numbers.
+  %We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
+  %which looks up the content of register $R$; if $R$
+  %is not in this list, then we return 0. Similarly we
+  %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.
 *}