src/HOL/List.thy
changeset 24308 700e745994c1
parent 24286 7619080e49f0
child 24335 21b4350cf5ec
     1.1 --- a/src/HOL/List.thy	Fri Aug 17 17:49:33 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Fri Aug 17 19:24:37 2007 +0200
     1.3 @@ -973,12 +973,9 @@
     1.4  lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
     1.5  by (induct xss) auto
     1.6  
     1.7 -lemma set_concat [simp]: "set (concat xs) = \<Union>(set ` set xs)"
     1.8 +lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
     1.9  by (induct xs) auto
    1.10  
    1.11 -lemma set_concat_map: "set(concat(map f xs)) = (UN x:set xs. set(f x))"
    1.12 -by(auto)
    1.13 -
    1.14  lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
    1.15  by (induct xs) auto
    1.16  
    1.17 @@ -2047,7 +2044,7 @@
    1.18  
    1.19  lemma length_remdups_concat:
    1.20   "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
    1.21 -by(simp add: distinct_card[symmetric])
    1.22 +by(simp add: set_concat distinct_card[symmetric])
    1.23  
    1.24  
    1.25  subsubsection {* @{text remove1} *}