equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 header {* Registration of Various Types as Bounded Natural Functors *} |
11 header {* Registration of Various Types as Bounded Natural Functors *} |
12 |
12 |
13 theory More_BNFs |
13 theory More_BNFs |
14 imports BNF_LFP BNF_GFP |
14 imports |
|
15 BNF_LFP |
|
16 BNF_GFP |
|
17 "~~/src/HOL/Quotient_Examples/FSet" |
|
18 "~~/src/HOL/Library/Multiset" |
|
19 Countable_Set |
15 begin |
20 begin |
16 |
21 |
17 lemma option_rec_conv_option_case: "option_rec = option_case" |
22 lemma option_rec_conv_option_case: "option_rec = option_case" |
18 by (simp add: fun_eq_iff split: option.split) |
23 by (simp add: fun_eq_iff split: option.split) |
19 |
24 |