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