# HG changeset patch
# User paulson
# Date 929608372 -7200
# Node ID 50459a995aa35125fd4bbf64db2f083112c7f6b4
# Parent  ea6832d74353be997c185903dfc4d280828a85dc
renamed UNION_o to UN_o (to fit the convention) and added image_UN, image_INT

diff -r ea6832d74353 -r 50459a995aa3 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Sun Jun 13 13:57:31 1999 +0200
+++ b/src/HOL/Fun.ML	Thu Jun 17 10:32:52 1999 +0200
@@ -60,7 +60,7 @@
 
 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
 by (Blast_tac 1);
-qed "UNION_o";
+qed "UN_o";
 
 
 section "inj";
@@ -221,6 +221,17 @@
 by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
 qed "inj_image_eq_iff";
 
+Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
+by (Blast_tac 1);
+qed "image_UN";
+
+(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
+Goalw [inj_on_def]
+   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
+\   ==> f `` (INTER A B) = (INT x:A. f `` B x)";
+by (Blast_tac 1);
+qed "image_INT";
+
 val set_cs = claset() delrules [equalityI];