Mercurial Mercurial > hg > tm / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 06 Feb 2013 04:32:18 +0000
changeset 132 264ff7014657
parent 131 e995ae949731
child 133 ca7fb6848715
updated
Paper/Paper.thy file | annotate | diff | comparison | revisions
paper.pdf file | annotate | diff | comparison | revisions 
--- a/Paper/Paper.thy	Wed Feb 06 04:27:03 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 04:32:18 2013 +0000
@@ -1322,7 +1322,7 @@
   which means that if the recursive function @{text r} with arguments @{text ns} evaluates
   to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started
   with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
-  with the standard tape @{term "(Bk \<up> l, <n::nat> @ Bk \<up> m)"} for some @{text l} and @{text m}.
+  with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
 
   and the also the definition of the
   universal function (we refer the reader to our formalisation).
Binary file paper.pdf has changed
tm