diff -r e0a7ee9842d6 -r ca2ea835c363 Paper/Paper.thy
--- a/Paper/Paper.thy	Fri Mar 29 02:40:38 2013 +0000
+++ b/Paper/Paper.thy	Mon Apr 01 18:15:00 2013 +0100
@@ -1577,8 +1577,8 @@
   \noindent
   If started with standard tape @{term "([], [Oc])"}, it halts with the
   non-standard tape @{term "([Oc, Bk], [])"} according to the definition in Chapter 3---so no
-  result is calculated; but with the standard tape @{term "([], [Oc])"} according to the 
-  definition in Chapter 8. ???? 
+  result is calculated; but with the standard tape @{term "([Bk], [Oc])"} according to the 
+  definition in Chapter 8. 
   We solve this inconsistency in our formalisation by
   setting up our definitions so that the @{text counter_example} Turing machine does not 
   produce any result by looping forever fetching @{term Nop}s in state @{text 0}.