equal
deleted
inserted
replaced
10 |
10 |
11 theory ListF |
11 theory ListF |
12 imports "../BNF" |
12 imports "../BNF" |
13 begin |
13 begin |
14 |
14 |
15 data (rep_compat) 'a listF = NilF | Conss 'a "'a listF" |
15 datatype_new (rep_compat) 'a listF = NilF | Conss 'a "'a listF" |
16 |
16 |
17 lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()" |
17 lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()" |
18 unfolding NilF_def listF.ctor_fold pre_listF_map_def by simp |
18 unfolding NilF_def listF.ctor_fold pre_listF_map_def by simp |
19 |
19 |
20 lemma fold_sum_case_Conss: |
20 lemma fold_sum_case_Conss: |