# HG changeset patch
# User nipkow
# Date 1187371477 -7200
# Node ID 700e745994c1454be54eb932fe769e6a494a26cb
# Parent  434c9fbc1787fe70a0b3e03b5fa0fabf7027afee
removed set_concat_map and improved set_concat

diff -r 434c9fbc1787 -r 700e745994c1 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 17 17:49:33 2007 +0200
+++ b/src/HOL/List.thy	Fri Aug 17 19:24:37 2007 +0200
@@ -973,12 +973,9 @@
 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) = \<Union>(set ` set xs)"
+lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
 by (induct xs) auto
 
-lemma set_concat_map: "set(concat(map f xs)) = (UN x:set xs. set(f x))"
-by(auto)
-
 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
 by (induct xs) auto
 
@@ -2047,7 +2044,7 @@
 
 lemma length_remdups_concat:
  "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
-by(simp add: distinct_card[symmetric])
+by(simp add: set_concat distinct_card[symmetric])
 
 
 subsubsection {* @{text remove1} *}