# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1362663665 0
# Node ID bfa2a8145f791fd234b42dbfbfbd81dcb3455d3e
# Parent  ebe8fd1fb26f99096b5b130bcb9eca1a95bd7351
tuned conclusion

diff -r ebe8fd1fb26f -r bfa2a8145f79 Paper/Paper.thy
--- 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
diff -r ebe8fd1fb26f -r bfa2a8145f79 paper.pdf
Binary file paper.pdf has changed