--- a/thys/Uncomputable.thy	Tue Feb 12 13:37:07 2013 +0000
+++ b/thys/Uncomputable.thy	Wed Feb 13 20:08:14 2013 +0000
@@ -987,13 +987,13 @@
 section {* The diagnal argument below shows the undecidability of Halting problem *}
 
 text {*
-  @{text "haltP tp x"} means TM @{text "tp"} terminates on input @{text "x"}
+  @{text "halts tp x"} means TM @{text "tp"} terminates on input @{text "x"}
   and the final configuration is standard.
 *}
 
-definition haltP :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
+definition halts :: "tprog0 \<Rightarrow> nat list \<Rightarrow> bool"
   where
-  "haltP p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"
+  "halts p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k,  <n::nat> @ Bk \<up> l)))}"
 
 lemma [intro, simp]: "tm_wf0 tcopy"
 by (auto simp: tcopy_def)
@@ -1021,9 +1021,9 @@
   The following two assumptions specifies that @{text "H"} does solve the Halting problem.
   *}
   and h_case: 
-  "\<And> M ns. haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
+  "\<And> M ns. halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>))}"
   and nh_case: 
-  "\<And> M ns. \<not> haltP M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}"
+  "\<And> M ns. \<not> halts M ns \<Longrightarrow> {(\<lambda>tp. tp = ([Bk], <(code M, ns)>))} H {(\<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>))}"
 begin
 
 (* invariants for H *)
@@ -1038,12 +1038,12 @@
 
 
 lemma H_halt_inv:
-  assumes "\<not> haltP M ns" 
+  assumes "\<not> halts M ns" 
   shows "{pre_H_inv M ns} H {post_H_halt_inv}"
 using assms nh_case by auto
 
 lemma H_unhalt_inv:
-  assumes "haltP M ns" 
+  assumes "halts M ns" 
   shows "{pre_H_inv M ns} H {post_H_unhalt_inv}"
 using assms h_case by auto
    
@@ -1056,7 +1056,7 @@
 
 (* assume tcontra does not halt on its code *)
 lemma tcontra_unhalt: 
-  assumes "\<not> haltP tcontra [code tcontra]"
+  assumes "\<not> halts tcontra [code tcontra]"
   shows "False"
 proof -
   (* invariants *)
@@ -1099,7 +1099,7 @@
 
   with assms show "False"
     unfolding P1_def P3_def
-    unfolding haltP_def
+    unfolding halts_def
     unfolding Hoare_halt_def 
     apply(auto)    
     apply(drule_tac x = n in spec)
@@ -1110,7 +1110,7 @@
 
 (* asumme tcontra halts on its code *)
 lemma tcontra_halt: 
-  assumes "haltP tcontra [code tcontra]"
+  assumes "halts tcontra [code tcontra]"
   shows "False"
 proof - 
   (* invariants *)
@@ -1152,7 +1152,7 @@
 
   with assms show "False"
     unfolding P1_def
-    unfolding haltP_def
+    unfolding halts_def
     unfolding Hoare_halt_def Hoare_unhalt_def
     by (auto simp add: tape_of_nl_abv)
 qed