| changeset 24461 | bbff04c027ec |
| parent 24449 | 2f05cb7fed85 |
| child 24471 | d7cf53c1085f |
--- a/src/HOL/List.thy Tue Aug 28 18:21:53 2007 +0200 +++ b/src/HOL/List.thy Tue Aug 28 18:23:59 2007 +0200 @@ -1004,7 +1004,7 @@ lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" by (induct xs) auto -lemma concat_map_singleton[simp, code]: "concat(map (%x. [f x]) xs) = map f xs" +lemma concat_map_singleton[simp, code unfold]: "concat(map (%x. [f x]) xs) = map f xs" by (induct xs) auto lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"