# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1364836500 -3600
# Node ID ca2ea835c363ece1bdbd7ac8ff84732b298b46a4
# Parent  e0a7ee9842d65c1dd285ac1f86143f249a0d641d
fixed counterexample according to def in Chap 8

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}. 
diff -r e0a7ee9842d6 -r ca2ea835c363 paper.pdf
Binary file paper.pdf has changed