equal
deleted
inserted
replaced
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 BNF_Wrap |
13 imports BNF_LFP BNF_GFP BNF_Wrap |
14 keywords |
14 keywords |
15 "data" :: thy_decl |
15 "data" :: thy_decl and |
16 and |
16 "codata" :: thy_decl and |
17 "codata" :: thy_decl |
17 "defaults" |
18 uses |
18 uses |
19 "Tools/bnf_fp_sugar_tactics.ML" |
19 "Tools/bnf_fp_sugar_tactics.ML" |
20 "Tools/bnf_fp_sugar.ML" |
20 "Tools/bnf_fp_sugar.ML" |
21 begin |
21 begin |
22 |
22 |