--- 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