Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Paper/Paper.thy
changeset 157 fe0e6733b9e4
parent 156 7c9dbacc6c7c
child 158 6a584d61820f
equal deleted inserted replaced
156:7c9dbacc6c7c 157:fe0e6733b9e4 
  1448   If started with standard tape @{term "([], [Oc])"}, it halts with the
 
  1448   If started with standard tape @{term "([], [Oc])"}, it halts with the
 
  1449   non-standard tape @{term "([Oc], [])"} according to the definition in Chapter 3---so no
 
  1449   non-standard tape @{term "([Oc], [])"} according to the definition in Chapter 3---so no
 
  1450   result is calculated; but with the standard tape @{term "([], [Oc])"} according to the 
  1450   result is calculated; but with the standard tape @{term "([], [Oc])"} according to the 
  1451   definition in Chapter 8. We solve this inconsitency in our formalisation by
 
  1451   definition in Chapter 8. We solve this inconsitency in our formalisation by
 
  1452   setting up our definitions so that the @{text counter_example} Turing machine does not 
  1452   setting up our definitions so that the @{text counter_example} Turing machine does not 
  1453   produce any result, but loops forever fetching @{term Nop}s in state @{text 0}. 
  1453   produce any result by looping forever fetching @{term Nop}s in state @{text 0}. 
  1454   
  1454   This solution is different from the definition in Chapter 3, but also 
       
  1455   different from the one in Chapter 8, where the instruction from state @{text 1} is 
       
  1456   fetched.
 
  1455 *}
 
  1457 *}
 
  1456 
  1458 
  1457 (*
 
  1459 (*
 
  1458 section {* XYZ *}
 
  1460 section {* XYZ *}
 
  1459 
  1461
tm