--- a/Paper/Paper.thy	Mon Feb 04 21:11:43 2013 +0000
+++ b/Paper/Paper.thy	Mon Feb 04 23:12:17 2013 +0000
@@ -221,7 +221,7 @@
 of register machines) and recursive functions. To see the difficulties
 involved with this work, one has to understand that Turing machine
 programs can be completely \emph{unstructured}, behaving similar to
-Basic programs containing the infamous goto-statement \cite{Dijkstra68}. This
+Basic programs containing the infamous goto-statements \cite{Dijkstra68}. This
 precludes in the general case a compositional Hoare-style reasoning
 about Turing programs.  We provide such Hoare-rules for when it
 \emph{is} possible to reason in a compositional manner (which is
@@ -1071,7 +1071,7 @@
   \end{center}
 
   \noindent
-  Suppose @{thm (prem 1) "tcontra_halt"}. Given the invariants on the 
+  Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants on the 
   left, we can derive the following Hoare-pair for @{term tcontra} on the right.
 
   \begin{center}\small
@@ -1098,11 +1098,11 @@
   This Hoare-pair contradicts our assumption that @{term tcontra} started
   with @{term "<(code tcontra)>"} halts.
 
-  Suppose @{thm (prem 1) "tcontra_unhalt"}. Again given the invariants on the 
+  Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again given the invariants on the 
   left, we can derive the Hoare-triple for @{term tcontra} on the right.
 
   \begin{center}\small
-  \begin{tabular}{@ {}c@ {\hspace{-17mm}}c@ {}}
+  \begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}}
   \begin{tabular}[t]{@ {}l@ {}}
   @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
   @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
@@ -1139,7 +1139,7 @@
   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; we also use a natural number
-  to represent a program counter. An abacus 
+  to represent a program counter and jumping ``addresses''. An abacus 
   program is a list of \emph{statements} defined by the datatype:
 
   \begin{center}
@@ -1162,7 +1162,7 @@
 
   \noindent
   Running such a program means we start with the first instruction
-  then execute statements one after the other, unless there is a jump.  For
+  then execute one statements 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