equal
deleted
inserted
replaced
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 Equiv_Relations_More |
11 imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Prefix_Order" |
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 |