add reference
authorAndreas Lochbihler
Tue Jan 12 15:23:54 2016 +0100 (2016-01-12)
changeset 6214100bfdf4bf237
parent 62140 c3a9dd69179e
child 62142 18a217591310
add reference
src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
     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>