--- a/Paper/Paper.thy	Tue Feb 12 13:37:07 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 13 20:08:14 2013 +0000
@@ -15,8 +15,7 @@
 
 consts DUMMY::'a
 
-
-(* THEOREMS *)
+(* Theorems as inference rules from LaTeXsugar.thy *)
 notation (Rule output)
   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
 
@@ -59,7 +58,6 @@
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
   update2 ("update") and
   tm_wf0 ("wf") and
-  (*is_even ("iseven") and*)
   tcopy_begin ("cbegin") and
   tcopy_loop ("cloop") and
   tcopy_end ("cend") and

--- a/thys/Rec_Def.thy	Tue Feb 12 13:37:07 2013 +0000
+++ b/thys/Rec_Def.thy	Wed Feb 13 20:08:14 2013 +0000
@@ -1,3 +1,10 @@
+(* Title: thys/Rec_Def.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Definition of Recursive Functions *}
+
+
 theory Rec_Def
 imports Main
 begin

--- a/thys/Recursive.thy	Tue Feb 12 13:37:07 2013 +0000
+++ b/thys/Recursive.thy	Wed Feb 13 20:08:14 2013 +0000
@@ -1,8 +1,13 @@
+(* Title: thys/Recursive.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Translating Recursive Functions into Abacus Machines *}
+
 theory Recursive
 imports Rec_Def Abacus
 begin
 
-section {* Compiling from recursive functions to Abacus machines *}
 
 text {*
   Some auxilliary Abacus machines used to construct the result Abacus machines.

--- a/thys/UF.thy	Tue Feb 12 13:37:07 2013 +0000
+++ b/thys/UF.thy	Wed Feb 13 20:08:14 2013 +0000
@@ -1,3 +1,9 @@
+(* Title: thys/UF.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Construction of a Universal Function *}
+
 theory UF
 imports Rec_Def GCD Abacus
 begin
@@ -9,7 +15,7 @@
   UTM can easil be obtained by compling @{text "rec_F"} into the corresponding Turing Machine.
 *}
 
-section {* Univeral Function *}
+section {* Universal Function *}
 
 subsection {* The construction of component functions *}
 

--- a/thys/UTM.thy	Tue Feb 12 13:37:07 2013 +0000
+++ b/thys/UTM.thy	Wed Feb 13 20:08:14 2013 +0000
@@ -1,3 +1,9 @@
+(* Title: thys/UTM.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+*)
+
+header {* Construction of a Universal Turing Machine *}
+
 theory UTM
 imports Recursive Abacus UF GCD Turing_Hoare
 begin
@@ -20,7 +26,7 @@
   compiled from @{text "rec_F"} as the second argument.
 
   However, this initialization TM (named @{text "t_wcode"}) can not be
-  constructed by compiling from any resurve function, because every
+  constructed by compiling from any recursive function, because every
   recursive function takes a fixed number of input arguments, while
   @{text "t_wcode"} needs to take varying number of arguments and
   tranform them into Wang's coding. Therefore, this section give a

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