changeset 49509 | 163914705f8d |
parent 49463 | 83ac281bcdc2 |
49508:1e205327f059 | 49509:163914705f8d |
---|---|
1 (* Title: HOL/Codatatype/BNF_Util.thy |
1 (* Title: HOL/BNF/BNF_Util.thy |
2 Author: Dmitriy Traytel, TU Muenchen |
2 Author: Dmitriy Traytel, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 Copyright 2012 |
4 Copyright 2012 |
5 |
5 |
6 Library for bounded natural functors. |
6 Library for bounded natural functors. |