# HG changeset patch
# User Andreas Lochbihler
# Date 1452608634 -3600
# Node ID 00bfdf4bf23706d25ff6b4603e79d4a776a772c6
# Parent  c3a9dd69179ede896a33c92db3d9641cdb72812f
add reference

diff -r c3a9dd69179e -r 00bfdf4bf237 src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
--- 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>