# HG changeset patch
# User paulson
# Date 877422983 -7200
# Node ID 7a38fae985f932332b997eedb5a5372b324a2f7e
# Parent  033633d9a0323953a57068214f009148f284d91c
New rewrite rules image_iff

diff -r 033633d9a032 -r 7a38fae985f9 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Mon Oct 20 17:21:54 1997 +0200
+++ b/src/HOL/Set.ML	Tue Oct 21 10:36:23 1997 +0200
@@ -623,6 +623,10 @@
 by (Blast_tac 1);
 qed "image_Un";
 
+goal Set.thy "(z : f``A) = (EX x:A. z = f x)";
+by (Blast_tac 1);
+qed "image_iff";
+
 
 (*** Range of a function -- just a translation for image! ***)