--- a/Paper/Paper.thy	Thu Mar 07 13:19:42 2013 +0000
+++ b/Paper/Paper.thy	Thu Mar 07 13:41:05 2013 +0000
@@ -1700,7 +1700,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 much smaller than for example the
+  relatively straightforward and 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
@@ -1711,7 +1711,7 @@
   Our reasoning about the invariants is not much supported by the
   automation beyond the standard automation tools available in Isabelle/HOL. 
   There is however a tantalising connection
-  between our work and very recent work \cite{Jensen13} on verifying
+  between our work and very recent work by Jensen et al \cite{Jensen13} on verifying
   X86 assembly code that might change that. They observed a similar phenomenon with assembly
   programs where Hoare-style reasoning is sometimes possible, but
   sometimes it is not. In order to ease their reasoning, they

Binary file paper.pdf has changed