changeset 49016 | 640ce226a973 |
parent 48975 | 7f79f94a432c |
child 49308 | 6190b701e4f4 |
49015:6b7cdb1f37d5 | 49016:640ce226a973 |
---|---|
7 |
7 |
8 header {* Composition of Bounded Natural Functors *} |
8 header {* Composition of Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_Comp |
10 theory BNF_Comp |
11 imports Basic_BNFs |
11 imports Basic_BNFs |
12 keywords |
|
13 "bnf_of_typ" :: thy_decl |
|
14 uses |
12 uses |
15 "Tools/bnf_comp_tactics.ML" |
13 "Tools/bnf_comp_tactics.ML" |
16 "Tools/bnf_comp.ML" |
14 "Tools/bnf_comp.ML" |
17 "Tools/bnf_fp_util.ML" |
15 "Tools/bnf_fp_util.ML" |
18 begin |
16 begin |