# HG changeset patch
# User paulson
# Date 889610730 -3600
# Node ID 6a7c70b053ccf17c0f3caec125255480a96caa64
# Parent  2c984ac036f5244d6caaab8b48e327f4d985a063
new theorem

diff -r 2c984ac036f5 -r 6a7c70b053cc src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Wed Mar 11 11:05:14 1998 +0100
+++ b/src/HOL/Vimage.ML	Wed Mar 11 11:05:30 1998 +0100
@@ -78,6 +78,11 @@
 qed "UN_vimage";
 Addsimps [UN_vimage];
 
+(*NOT suitable for rewriting*)
+goal thy "f-``B = (UN y: B. f-``{y})";
+by (Blast_tac 1);
+qed "vimage_eq_UN";
+
 
 (** monotonicity **)