# HG changeset patch
# User paulson
# Date 940252570 -7200
# Node ID 1b3b683c092e5d4c9af8484383ee9cdb9c5c8e28
# Parent  1baf422ec16a328f2a043f83b8299baa7d1737a6
new thm vimage_image_eq

diff -r 1baf422ec16a -r 1b3b683c092e src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Sat Oct 16 18:56:09 1999 +0200
+++ b/src/HOL/Fun.ML	Mon Oct 18 15:16:10 1999 +0200
@@ -253,6 +253,10 @@
 qed "vimage_id";
 Addsimps [vimage_ident, vimage_id];
 
+Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}";
+by (blast_tac (claset() addIs [sym]) 1);
+qed "vimage_image_eq";
+
 Goal "f``(A Int B) <= f``A Int f``B";
 by (Blast_tac 1);
 qed "image_Int_subset";