| changeset 49074 | d8af889dcbe3 |
| parent 49020 | f379cf5d71bd |
| child 49075 | ed769978dc8d |
| 49073:88fe93ae61cf | 49074:d8af889dcbe3 |
|---|---|
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_LFP BNF_GFP |
14 keywords |
14 keywords |
15 "bnf_sugar" :: thy_goal |
15 "wrap_data" :: thy_goal |
16 uses |
16 usesy |
17 "Tools/bnf_sugar_tactics.ML" |
17 "Tools/bnf_wrap_tactics.ML" |
18 "Tools/bnf_sugar.ML" |
18 "Tools/bnf_wrap.ML" |
19 begin |
19 begin |
20 |
20 |
21 end |
21 end |