# HG changeset patch
# User paulson
# Date 940610460 -7200
# Node ID 3cb310f40a3a193476c11c791a4c6342cda361e8
# Parent  c7fd7eb3b0efa0e8d34c87420f3d627c6f42de00
replaced image_image_eq_UN by image_eq_UN

diff -r c7fd7eb3b0ef -r 3cb310f40a3a src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Oct 22 18:35:20 1999 +0200
+++ b/src/HOL/Fun.ML	Fri Oct 22 18:41:00 1999 +0200
@@ -67,9 +67,9 @@
 by (Blast_tac 1);
 qed "image_compose";
 
-Goal "f``g``A = (UN x:A. {f (g x)})";
+Goal "f``A = (UN x:A. {f x})";
 by (Blast_tac 1);
-qed "image_image_eq_UN";
+qed "image_eq_UN";
 
 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
 by (Blast_tac 1);