| changeset 48975 | 7f79f94a432c |
| child 49282 | c057e1b39f16 |
| 48974:8882fc8005ad | 48975:7f79f94a432c |
|---|---|
1 (* Title: HOL/Codatatype/BNF_Def.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Definition of bounded natural functors. |
|
6 *) |
|
7 |
|
8 header {* Definition of Bounded Natural Functors *} |
|
9 |
|
10 theory BNF_Def |
|
11 imports BNF_Library |
|
12 keywords |
|
13 "print_bnfs" :: diag |
|
14 and |
|
15 "bnf_def" :: thy_goal |
|
16 uses |
|
17 "Tools/bnf_util.ML" |
|
18 "Tools/bnf_tactics.ML" |
|
19 "Tools/bnf_def.ML" |
|
20 begin |
|
21 |
|
22 end |