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.
 *}
 
 (*