--- a/Paper/Paper.thy	Thu Feb 07 00:48:09 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 00:50:19 2013 +0000
@@ -1178,7 +1178,7 @@
   \noindent
   Running such a program means we start with the first instruction
   then execute one instructions after the other, unless there is a jump.  For
-  example the second instruction @{term "Goto 0"} means
+  example the second instruction @{term "Goto 0"} above means
   we jump back to the first instruction thereby closing the loop.  Like with our
   Turing machines, we fetch instructions from an abacus program such
   that a jump out of ``range'' behaves like a @{term "Nop"}-action. In