diff -r 641512ab0f6c -r d7570dbf9f06 thys/Uncomputable.thy
--- a/thys/Uncomputable.thy	Mon Feb 11 08:46:24 2013 +0000
+++ b/thys/Uncomputable.thy	Tue Feb 12 13:37:07 2013 +0000
@@ -1,9 +1,8 @@
-(* Title: Turing machine's definition and its charater
-   Author: XuJian <xujian817@hotmail.com>
-   Maintainer: Xujian
+(* Title: thys/Uncomputable.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Undeciablity of the {\em Halting problem} *}
+header {* Undeciablity of the Halting Problem *}
 
 theory Uncomputable
 imports Turing_Hoare
@@ -19,12 +18,10 @@
   and "7 = Suc 6"
   and "8 = Suc 7" 
   and "9 = Suc 8" 
-  and "10 = Suc 9" 
-  by arith+
+  and "10 = Suc 9"
+by simp_all
 
-text {*
-  The {\em Copying} TM, which duplicates its input. 
-*}
+text {* The Copying TM, which duplicates its input. *}
 
 definition 
   tcopy_begin :: "instr list"
@@ -88,7 +85,7 @@
   shows "inv_begin n (step0 cf tcopy_begin)"
 using assms
 unfolding tcopy_begin_def
-apply(case_tac cf)
+apply(cases cf)
 apply(auto simp: numeral split: if_splits)
 apply(case_tac "hd c")
 apply(auto)