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