# HG changeset patch
# User paulson
# Date 939631841 -7200
# Node ID 742715638a0127000b136ecc5662095bf3623dea
# Parent  09aabe6d04b8d8499f38d6759f13590cf3f205f9
new thm vimage_INT; deleted redundant UN_vimage

diff -r 09aabe6d04b8 -r 742715638a01 src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Mon Oct 11 10:49:18 1999 +0200
+++ b/src/HOL/Vimage.ML	Mon Oct 11 10:50:41 1999 +0200
@@ -63,6 +63,10 @@
 by (Blast_tac 1);
 qed "vimage_UN";
 
+Goal "f-``(INT x:A. B x) = (INT x:A. f -`` B x)";
+by (Blast_tac 1);
+qed "vimage_INT";
+
 bind_thm ("vimage_Collect", allI RS prove_goalw thy [vimage_def]
   "! x. P (f x) = Q x ==> f -`` (Collect P) = Collect Q"
     (fn prems => [cut_facts_tac prems 1, Fast_tac 1]));
@@ -83,11 +87,6 @@
 qed "vimage_UNIV";
 Addsimps [vimage_UNIV];
 
-Goal "(UN x:A. f -`` B x) = f -`` (UN x:A. B x)";
-by (Blast_tac 1);
-qed "UN_vimage";
-Addsimps [UN_vimage];
-
 (*NOT suitable for rewriting*)
 Goal "f-``B = (UN y: B. f-``{y})";
 by (Blast_tac 1);