src/HOL/List.thy
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"