| changeset 51804 | be6e703908f4 |
| parent 49634 | 9a21861a2d5c |
| child 53353 | 0c1c67e3fccc |
--- a/src/HOL/BNF/Examples/ListF.thy Mon Apr 29 06:13:36 2013 +0200 +++ b/src/HOL/BNF/Examples/ListF.thy Mon Apr 29 09:10:49 2013 +0200 @@ -12,7 +12,7 @@ imports "../BNF" begin -data (rep_compat) 'a listF = NilF | Conss 'a "'a listF" +datatype_new (rep_compat) 'a listF = NilF | Conss 'a "'a listF" lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()" unfolding NilF_def listF.ctor_fold pre_listF_map_def by simp