equal
deleted
inserted
replaced
9 |
9 |
10 header {* Registration of Basic Types as Bounded Natural Functors *} |
10 header {* Registration of Basic Types as Bounded Natural Functors *} |
11 |
11 |
12 theory Basic_BNFs |
12 theory Basic_BNFs |
13 imports BNF_Def |
13 imports BNF_Def |
14 (*FIXME: define relators here, reuse in Lifting_* once this theory is in HOL*) |
|
15 begin |
14 begin |
16 |
15 |
17 bnf ID: 'a |
16 bnf ID: 'a |
18 map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
17 map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
19 sets: "\<lambda>x. {x}" |
18 sets: "\<lambda>x. {x}" |