--- a/Paper/Paper.thy	Tue Feb 05 10:12:56 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 05 10:23:08 2013 +0000
@@ -1181,7 +1181,8 @@
   standard tapes. Because of the jumps in abacus programs, it
   seems difficult to build a Turing machine programs out of components 
   using our @{text "\<oplus>"}-operation shown in the previous section.
-  To overcome this difficulty, we calculate a \emph{layout} as follows
+  To overcome this difficulty, we calculate a \emph{layout} of an
+  abacus program as follows
 
   \begin{center}
   \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
@@ -1203,8 +1204,8 @@
   \end{center}
 
   \noindent
-  where @{term "i"} is the corresponding state in the Turing machine program 
-  to jump to. For translating the instruction @{term Inc}
+  where @{term "i"} is the state in the Turing machine program 
+  to jump to. For translating the instruction @{term Inc}, 
   one has to remember that the content of the registers are encoded
   in the Turing machine as standard tape. Therefore the translated Turing machine 
   needs to first find the number corresponding to the register @{text "R"}. This needs a machine
@@ -1220,15 +1221,15 @@
 
   \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''. By adjusting we only need to 
   replace the first @{term Oc} of each number by @{term Bk} and the last
   one from @{term Bk} to @{term Oc}.
-  Finally we need to transition the head of the
+  Finally, we need to transition the head of the
   Turing machine back into the standard position. This requires a Turing machine
   with 9 states (we omit the details). Similarly for the translation of @{term Dec}, where the 
   translated Turing machine needs to first check whether the content of the
   corresponding register is @{text 0}. For this we have a Turing machine program
-  with @{text 16} states. 
+  with @{text 16} states (again details are omitted). 
 
   Finally, having a Turing machine for each abacus instruction we need
   to ``stitch'' the Turing machines together into one so that each
@@ -1237,22 +1238,21 @@
   program is assumed to calculate a value stored in the last
   register. That means we have to append a Turing machine that
   ``mops up'' the tape (cleaning all @{text Oc}s) except for the
-  last number represented on the tape.
+  @{term Oc}s of the last number represented on the tape.
 
-  While generating the Turing machine program for an abacus
-  program is not too difficult to formalise, the problem is that it
-  contains @{text Goto}s all over the place. The unfortunate result is
-  are needed to translate each abacus instruction that we cannot
-  use our Hoare-rules for reasoning about sequentially composed
-  programs. Instead we have to treat the Turing machine as one
-  are needed to translate each abacus instruction``block''
-  and show as invariant that it performs the same operations
-  as the abacus program. For this we have to show that for each
-  configuration of an abacus machine the @{term step}-function
-  is simulated by zero or more steps in our constructed Turing
-  machine. This leads to a rather large ``monolithic'' 
-  correctness proof (4600 loc and 380 sublemmas) that on the conceptual 
-  level is difficult to break down into smaller components. 
+  While generating the Turing machine program for an abacus program is
+  not too difficult to formalise, the problem is that it contains
+  @{text Goto}s all over the place. The unfortunate result is that we
+  cannot use our Hoare-rules for reasoning about sequentially composed
+  programs (for this the programs need to be independent). Instead we
+  have to treat the translated Turing machine as one ``big block'' and 
+  prove as invariant that it performs
+  the same operations as the abacus program. For this we have to show
+  that for each configuration of an abacus machine the @{term
+  step}-function is simulated by zero or more steps in our translated
+  Turing machine. This leads to a rather large ``monolithic''
+  correctness proof (4600 loc and 380 sublemmas) that on the
+  conceptual level is difficult to break down into smaller components.
   
   %We were able to simplify the proof somewhat
 *}