changeset 69276 | 3d954183b707 |
parent 69275 | 9bbd5497befd |
child 69312 | e0f68a507683 |
--- a/src/HOL/List.thy Sat Nov 10 07:57:19 2018 +0000 +++ b/src/HOL/List.thy Sat Nov 10 07:57:20 2018 +0000 @@ -1633,7 +1633,7 @@ lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])" by (induct xss) auto -lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" +lemma set_concat [simp]: "set (concat xs) = (\<Union>x\<in>set xs. set x)" by (induct xs) auto lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"