changeset 49313 | 3f8671b353ae |
parent 49312 | c874ff5658dc |
child 49314 | f252c7c2ac7b |
49312:c874ff5658dc | 49313:3f8671b353ae |
---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Greatest Fixed Point Operation on Bounded Natural Functors *} |
8 header {* Greatest Fixed Point Operation on Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_GFP |
10 theory BNF_GFP |
11 imports BNF_FP |
11 imports BNF_FP Equiv_Relations_More |
12 keywords |
12 keywords |
13 "codata_raw" :: thy_decl and |
13 "codata_raw" :: thy_decl and |
14 "codata" :: thy_decl |
14 "codata" :: thy_decl |
15 begin |
15 begin |
16 |
16 |