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