--- a/Paper/Paper.thy	Sun Feb 03 13:31:14 2013 +0000
+++ b/Paper/Paper.thy	Mon Feb 04 01:17:09 2013 +0000
@@ -1117,7 +1117,7 @@
   This time the Hoare-triple states that @{term tcontra} terminates 
   with the ``output'' @{term "<(1::nat)>"}. In both case we come
   to an contradiction, which means we have to abondon our assumption 
-  that there exists a Turing machine @{term H} which can decide 
+  that there exists a Turing machine @{term H} which can in general decide 
   whether Turing machines terminate.
 *}
 
@@ -1126,14 +1126,13 @@
 
 text {*
   \noindent
-  Boolos et al \cite{Boolos87} use abacus machines as a 
-  stepping stone for making it less laborious to write
-  programs for Turing machines. Abacus machines operate
-  over an unlimited number 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
+  Boolos et al \cite{Boolos87} use abacus machines as a stepping stone
+  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
 
   \begin{center}
   \begin{tabular}{rcl@ {\hspace{10mm}}l}
@@ -1148,15 +1147,15 @@
   \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 0) can be defined as follows:
+  $R$ (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]}
+  @{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 opcode, namely @{text "Dec R o"}.
+  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>"},