| changeset 49075 | ed769978dc8d |
| parent 49074 | d8af889dcbe3 |
| child 49112 | 4de4635d8f93 |
| 49074:d8af889dcbe3 | 49075:ed769978dc8d |
|---|---|
8 *) |
8 *) |
9 |
9 |
10 header {* The (Co)datatype Package *} |
10 header {* The (Co)datatype Package *} |
11 |
11 |
12 theory Codatatype |
12 theory Codatatype |
13 imports BNF_LFP BNF_GFP |
13 imports BNF_Wrap BNF_LFP BNF_GFP |
14 keywords |
|
15 "wrap_data" :: thy_goal |
|
16 usesy |
|
17 "Tools/bnf_wrap_tactics.ML" |
|
18 "Tools/bnf_wrap.ML" |
|
19 begin |
14 begin |
20 |
15 |
21 end |
16 end |