diff -r c56f04b6a2f9 -r 07730607b0ca Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 07 00:50:19 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 01:00:55 2013 +0000
@@ -1211,13 +1211,13 @@
   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 program
-  code of one abacus instruction ends.
+  code of one abacus instruction ends and the next starts.
   The @{text Goto}
   instruction is easiest to translate requiring only one state, namely
   the Turing machine program:
 
   \begin{center}
-  @{text "tm_of_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]}
+  @{text "translate_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]}
   \end{center}
 
   \noindent
@@ -1239,7 +1239,7 @@
 
   \noindent
   Then we need to increase the ``number'' on the tape by one,
-  and adjust the following ``registers''. By adjusting we only need to 
+  and adjust the following ``registers''. For adjusting we only need to 
   change the first @{term Oc} of each number to @{term Bk} and the last
   one from @{term Bk} to @{term Oc}.
   Finally, we need to transition the head of the
@@ -1287,7 +1287,7 @@
   function for Church numbers, and also from Asperti and Ricciotti 
   \cite{AspertiRicciotti12} who construct a universal Turing machine
   directly, but for simulating Turing machines with a more restricted alphabet.
-  \emph{Recursive functions} @{term r} are defined as the datatype
+  \emph{Recursive functions} are defined as the datatype
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{4mm}}c}
@@ -1314,16 +1314,17 @@
   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 the following
-  theorem about the translation: Assuming 
+  theorem about the translation: If 
   @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
-  then the following Hoare-triple holds
+  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"]}
   \end{center}
 
   \noindent
-  which means that if the recursive function @{text r} with arguments @{text ns} evaluates
+  for the Turing machine. This
+  means that if the recursive function @{text r} with arguments @{text ns} evaluates
   to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started
   with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
   with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.