# HG changeset patch
# User paulson
# Date 919158635 -3600
# Node ID e3096df443264ae7cfd25da2012dfc8eb7dc83a9
# Parent  589671bebbb37ef5aaa1928dcbf0f6cb438a2386
new theorem image_Union_eq

diff -r 589671bebbb3 -r e3096df44326 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Sat Feb 13 22:08:54 1999 +0100
+++ b/src/HOL/equalities.ML	Tue Feb 16 10:50:35 1999 +0100
@@ -502,6 +502,10 @@
 by (Blast_tac 1);
 qed "Union_image_eq";
 
+Goal "f `` Union S = (UN x:S. f `` x)";
+by (Blast_tac 1);
+qed "image_Union_eq";
+
 Goal "Inter(B``A) = (INT x:A. B(x))";
 by (Blast_tac 1);
 qed "Inter_image_eq";