equal
deleted
inserted
replaced
48 lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" by auto |
48 lift_definition concat :: "'a dlist dlist \<Rightarrow> 'a dlist" is "remdups o List.concat" by auto |
49 |
49 |
50 text \<open>We can export code:\<close> |
50 text \<open>We can export code:\<close> |
51 |
51 |
52 export_code empty insert remove map filter null member length fold foldr concat in SML |
52 export_code empty insert remove map filter null member length fold foldr concat in SML |
|
53 file_prefix dlist |
53 |
54 |
54 end |
55 end |