--- a/Paper/Paper.thy	Wed Feb 13 20:08:14 2013 +0000
+++ b/Paper/Paper.thy	Thu Feb 14 09:31:19 2013 +0000
@@ -66,7 +66,6 @@
   code_tcontra ("code contra") and
   steps0 ("steps") and
   exponent ("_\<^bsup>_\<^esup>") and
-  haltP ("halts") and 
   tcopy ("copy") and 
   tape_of ("\<langle>_\<rangle>") and 
   tm_comp ("_ \<oplus> _") and 
@@ -1045,7 +1044,7 @@
   number is defined as
 
   \begin{center}
-  @{thm haltP_def}
+  @{thm halts_def}
   \end{center}
 
   \noindent