--- a/Paper/Paper.thy	Thu Feb 21 16:07:40 2013 +0000
+++ b/Paper/Paper.thy	Fri Feb 22 14:31:34 2013 +0000
@@ -1220,7 +1220,10 @@
   This gives us a list of natural numbers specifying how many states
   are needed to translate each abacus instruction. This information
   is needed in order to calculate the state where the Turing machine program
-  of one abacus instruction ends and the next starts.
+  of one abacus instruction starts. 
+
+  {\it add something here about address}
+
   The @{text Goto}
   instruction is easiest to translate requiring only one state, namely
   the Turing machine program:
@@ -1315,17 +1318,19 @@
 
   \noindent 
   where @{text n} indicates the function expects @{term n} arguments
-  (@{text z} and @{term s} expect one argument), and @{text rs} stands
-  for a list of recursive functions. Since we know in each case 
-  the arity, say @{term l}, we can define an inductive evaluation relation that  
-  relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l},
-  to what the result of the recursive function is, say @{text n}. We omit the
-  definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the 
-  definition of translating
-  recursive functions into abacus programs. We can prove, however,  the following
-  theorem about the translation: If 
-  @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
-  holds for the recursive function @{text r}, then the following Hoare-triple holds
+  (in \cite{Boolos87} both @{text z} and @{term s} expect one
+  argument), and @{text rs} stands for a list of recursive
+  functions. Since we know in each case the arity, say @{term l}, we
+  can define an inductive evaluation relation that relates a recursive
+  function @{text r} and a list @{term ns} of natural numbers of
+  length @{text l}, to what the result of the recursive function is,
+  say @{text n}. We omit the definition of @{term "rec_calc_rel r ns
+  n"}. Because of space reasons, we also omit the definition of
+  translating recursive functions into abacus programs. We can prove,
+  however, the following theorem about the translation: If @{thm (prem
+  1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and
+  r="n"]} holds for the recursive function @{text r}, then the
+  following Hoare-triple holds
 
   \begin{center}
   @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}