# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1360125138 0
# Node ID 264ff70146578309d94dc6f98cc2ddd27061d50c
# Parent  e995ae949731bc05cfeb465ac039d4d36c0a17bb
updated

diff -r e995ae949731 -r 264ff7014657 Paper/Paper.thy
--- 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).
diff -r e995ae949731 -r 264ff7014657 paper.pdf
Binary file paper.pdf has changed