src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
changeset 62141 00bfdf4bf237
parent 62058 1cfd5d604937
child 62390 842917225d56
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 12 15:21:34 2016 +0100
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 12 15:23:54 2016 +0100
@@ -1,5 +1,8 @@
 (*  Title:      HOL/Library/Bourbaki_Witt_Fixpoint.thy
     Author:     Andreas Lochbihler, ETH Zurich
+
+  Follows G. Smolka, S. Schäfer and C. Doczkal: Transfinite Constructions in
+  Classical Type Theory. ITP 2015
 *)
 
 section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>