--- 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:
--- 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