updated paper
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 07 Feb 2013 05:23:53 +0000
changeset 157 fe0e6733b9e4
parent 156 7c9dbacc6c7c
child 158 6a584d61820f
updated paper
Paper/Paper.thy
paper.pdf
--- 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.
 *}
 
 (*
Binary file paper.pdf has changed