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

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

Binary file paper.pdf has changed