| changeset 55075 | b3d0a02a756d |
| parent 55074 | 2b0b6f69b148 |
| child 55076 | 1e73e090a514 |
| 55074:2b0b6f69b148 | 55075:b3d0a02a756d |
|---|---|
1 (* Title: HOL/BNF/BNF.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 Copyright 2012 |
|
6 |
|
7 Bounded natural functors for (co)datatypes. |
|
8 *) |
|
9 |
|
10 header {* Bounded Natural Functors for (Co)datatypes *} |
|
11 |
|
12 theory BNF |
|
13 imports More_BNFs Countable_Set_Type BNF_Decl |
|
14 begin |
|
15 |
|
16 end |