diff -r 93db7414931d -r 293e9c6f22e1 thys/Recursive.thy
--- a/thys/Recursive.thy	Fri Dec 21 15:30:24 2018 +0100
+++ b/thys/Recursive.thy	Mon Jan 07 13:44:19 2019 +0100
@@ -1,3 +1,8 @@
+(* Title: thys/Recursive.thy
+   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
+   Modifications: Sebastiaan Joosten
+*)
+
 theory Recursive
 imports Abacus Rec_Def Abacus_Hoare
 begin