# HG changeset patch
# User haftmann
# Date 1316549482 -7200
# Node ID 05031b71a89a1ea9ef698e238113c0bfe241abce
# Parent  060f76635bfee17c6b38c584b466db3f9e92bf15
official status for UN_singleton

diff -r 060f76635bfe -r 05031b71a89a NEWS
--- a/NEWS	Tue Sep 20 21:47:52 2011 +0200
+++ b/NEWS	Tue Sep 20 22:11:22 2011 +0200
@@ -91,8 +91,7 @@
 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
-UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
-discarded.
+UNION_eq_Union_image, Union_def, UN_eq have been discarded.
 
 More consistent and comprehensive names:
 
diff -r 060f76635bfe -r 05031b71a89a src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Sep 20 21:47:52 2011 +0200
+++ b/src/HOL/Complete_Lattices.thy	Tue Sep 20 22:11:22 2011 +0200
@@ -1012,6 +1012,9 @@
 lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
   by blast
 
+lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
+  by blast
+
 
 subsection {* Distributive laws *}
 
@@ -1131,11 +1134,6 @@
   "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
   by auto
 
-text {* Legacy names *}
-
-lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
-  by blast
-
 text {* Finally *}
 
 no_notation