src/HOL/Set.thy
changeset 29691 9f03b5f847cd
parent 28562 4e74209f113e
child 29901 f4b3f8fbf599
     1.1 --- a/src/HOL/Set.thy	Thu Jan 29 22:27:07 2009 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Jan 29 22:28:03 2009 +0100
     1.3 @@ -885,6 +885,10 @@
     1.4      "A = B ==> (!!x. x:B ==> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
     1.5    by (simp add: UNION_def)
     1.6  
     1.7 +lemma strong_UN_cong:
     1.8 +    "A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
     1.9 +  by (simp add: UNION_def simp_implies_def)
    1.10 +
    1.11  
    1.12  subsubsection {* Intersections of families *}
    1.13