equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Bourbaki_Witt_Fixpoint.thy |
1 (* Title: HOL/Library/Bourbaki_Witt_Fixpoint.thy |
2 Author: Andreas Lochbihler, ETH Zurich |
2 Author: Andreas Lochbihler, ETH Zurich |
|
3 |
|
4 Follows G. Smolka, S. Schäfer and C. Doczkal: Transfinite Constructions in |
|
5 Classical Type Theory. ITP 2015 |
3 *) |
6 *) |
4 |
7 |
5 section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close> |
8 section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close> |
6 |
9 |
7 theory Bourbaki_Witt_Fixpoint imports Main begin |
10 theory Bourbaki_Witt_Fixpoint imports Main begin |