Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add reference
authorAndreas Lochbihler
Tue, 12 Jan 2016 15:23:54 +0100
changeset 62141 00bfdf4bf237
parent 62140 c3a9dd69179e
child 62142 18a217591310
add reference
src/HOL/Library/Bourbaki_Witt_Fixpoint.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle