diff -r d7570dbf9f06 -r 6013ca0e6e22 thys/UF.thy
--- 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 *}