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