changeset 57698 | afef6616cbae |
parent 56166 | 9a241bc276cd |
57697:44341963ade3 | 57698:afef6616cbae |
---|---|
1 (* Title: HOL/BNF_Comp.thy |
1 (* Title: HOL/BNF_Comp.thy |
2 Author: Dmitriy Traytel, TU Muenchen |
2 Author: Dmitriy Traytel, TU Muenchen |
3 Copyright 2012 |
3 Author: Jasmin Blanchette, TU Muenchen |
4 Copyright 2012, 2013, 2014 |
|
4 |
5 |
5 Composition of bounded natural functors. |
6 Composition of bounded natural functors. |
6 *) |
7 *) |
7 |
8 |
8 header {* Composition of Bounded Natural Functors *} |
9 header {* Composition of Bounded Natural Functors *} |