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