official status for UN_singleton
authorhaftmann
Tue Sep 20 22:11:22 2011 +0200 (2011-09-20)
changeset 4501305031b71a89a
parent 45012 060f76635bfe
child 45016 a5d43ffc95eb
official status for UN_singleton
NEWS
src/HOL/Complete_Lattices.thy
     1.1 --- a/NEWS	Tue Sep 20 21:47:52 2011 +0200
     1.2 +++ b/NEWS	Tue Sep 20 22:11:22 2011 +0200
     1.3 @@ -91,8 +91,7 @@
     1.4  Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
     1.5  INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
     1.6  INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
     1.7 -UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
     1.8 -discarded.
     1.9 +UNION_eq_Union_image, Union_def, UN_eq have been discarded.
    1.10  
    1.11  More consistent and comprehensive names:
    1.12  
     2.1 --- a/src/HOL/Complete_Lattices.thy	Tue Sep 20 21:47:52 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Sep 20 22:11:22 2011 +0200
     2.3 @@ -1012,6 +1012,9 @@
     2.4  lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
     2.5    by blast
     2.6  
     2.7 +lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
     2.8 +  by blast
     2.9 +
    2.10  
    2.11  subsection {* Distributive laws *}
    2.12  
    2.13 @@ -1131,11 +1134,6 @@
    2.14    "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
    2.15    by auto
    2.16  
    2.17 -text {* Legacy names *}
    2.18 -
    2.19 -lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
    2.20 -  by blast
    2.21 -
    2.22  text {* Finally *}
    2.23  
    2.24  no_notation