# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1357802428 0
# Node ID 7971da47e8c495d783d28f803af3d044a32071d6
# Parent  a961c2e4dcea9bf2d9d8e4f7685d2f9afb25897d
added

diff -r a961c2e4dcea -r 7971da47e8c4 Paper.thy
--- a/Paper.thy	Thu Jan 10 01:46:51 2013 +0000
+++ b/Paper.thy	Thu Jan 10 07:20:28 2013 +0000
@@ -323,6 +323,8 @@
   For showing the undecidability of the halting problem, we need to consider
   two specific Turing machines.
   
+
+  No evaluator in HOL, because of totality.
 *}
 
 section {* Abacus Machines *}
diff -r a961c2e4dcea -r 7971da47e8c4 document/root.tex
--- a/document/root.tex	Thu Jan 10 01:46:51 2013 +0000
+++ b/document/root.tex	Thu Jan 10 07:20:28 2013 +0000
@@ -45,7 +45,7 @@
 prover is to formalise a concrete model for computation. 
 We formalise Turing machines and relate them to abacus machines and recursive
 functions. Our theory can be used to formalise other computability results:
-we give one example about the undecidability of Wang tilings, whose proof uses
+we give one example about the undecidability of Wang's tiling problem, whose proof uses
 the notion of a universal Turing machine.
 \end{abstract}
 
diff -r a961c2e4dcea -r 7971da47e8c4 paper.pdf
Binary file paper.pdf has changed