src/HOL/equalities.ML

--- a/src/HOL/equalities.ML	Thu Aug 06 18:21:14 1998 +0200
+++ b/src/HOL/equalities.ML	Sat Aug 08 14:00:56 1998 +0200
@@ -123,6 +123,11 @@
 qed "image_is_empty";
 AddIffs [image_is_empty];
 
+Goal "f `` {x. P x} = {f x | x. P x}";
+by(Blast_tac 1);
+qed "image_Collect";
+Addsimps [image_Collect];
+
 Goalw [image_def]
 "(%x. if P x then f x else g x) `` S                    \
 \ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";