equal
deleted
inserted
replaced
12 imports Main |
12 imports Main |
13 begin |
13 begin |
14 |
14 |
15 datatype_new 'a listF (map: mapF rel: relF) = |
15 datatype_new 'a listF (map: mapF rel: relF) = |
16 NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF") |
16 NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF") |
17 datatype_new_compat listF |
17 datatype_compat listF |
18 |
18 |
19 definition Singll ("[[_]]") where |
19 definition Singll ("[[_]]") where |
20 [simp]: "Singll a \<equiv> Conss a NilF" |
20 [simp]: "Singll a \<equiv> Conss a NilF" |
21 |
21 |
22 primrec appendd (infixr "@@" 65) where |
22 primrec appendd (infixr "@@" 65) where |