changeset 55210 | d1e3b708d74b |
parent 55197 | 5a54ed681ba2 |
child 56016 | 8875cdcfc85b |
55209:bfafffd5421d | 55210:d1e3b708d74b |
---|---|
1 (* Title: HOL/BNF/Tools/bnf_decl.ML |
1 (* Title: HOL/Library/bnf_decl.ML |
2 Author: Dmitriy Traytel, TU Muenchen |
2 Author: Dmitriy Traytel, TU Muenchen |
3 Copyright 2013 |
3 Copyright 2013 |
4 |
4 |
5 Axiomatic declaration of bounded natural functors. |
5 Axiomatic declaration of bounded natural functors. |
6 *) |
6 *) |