# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360214633 0
# Node ID fe0e6733b9e4074b7134205efdda3c12078a1bd8
# Parent  7c9dbacc6c7c8d2c1dd0c979023b741279f08c24
updated paper

diff -r 7c9dbacc6c7c -r fe0e6733b9e4 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Feb 07 05:19:01 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 07 05:23:53 2013 +0000
@@ -1450,8 +1450,10 @@
   result is calculated; but with the standard tape @{term "([], [Oc])"} according to the 
   definition in Chapter 8. We solve this inconsitency in our formalisation by
   setting up our definitions so that the @{text counter_example} Turing machine does not 
-  produce any result, but loops forever fetching @{term Nop}s in state @{text 0}. 
-  
+  produce any result by looping forever fetching @{term Nop}s in state @{text 0}. 
+  This solution is different from the definition in Chapter 3, but also 
+  different from the one in Chapter 8, where the instruction from state @{text 1} is 
+  fetched.
 *}
 
 (*
diff -r 7c9dbacc6c7c -r fe0e6733b9e4 paper.pdf
Binary file paper.pdf has changed