diff -r 49dcc0b9b0b3 -r b66578c08490 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Mar 27 13:16:37 2013 +0000
+++ b/Paper/Paper.thy	Wed Mar 27 13:24:41 2013 +0000
@@ -1672,7 +1672,8 @@
   \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to
   some slick mechanised proofs, our experience is that Turing machines
   are not too daunting if one is only concerned with formalising the
-  undecidability of the halting problem for Turing machines.  This
+  undecidability of the halting problem for Turing machines.  As a point of 
+  comparison, the halting problem
   took us around 1500 loc of Isar-proofs, which is just one-and-a-half
   times of a mechanised proof pearl about the Myhill-Nerode
   theorem. So our conclusion is that this part is not as daunting 
@@ -1705,7 +1706,7 @@
   with the task of finding appropriate invariants and measures for
   showing the correctness and termination of these Turing machines.
   Whenever we can use Hoare-style reasoning, the invariants are
-  relatively straightforward and as a point of comparison much smaller than for example the
+  relatively straightforward and again as a point of comparison much smaller than for example the
   invariants used by Myreen in a correctness proof of a garbage collector
   written in machine code \cite[Page 76]{Myreen09}. However, the invariant 
   needed for the abacus proof, where Hoare-style reasoning does not work, is