# HG changeset patch
# User paulson
# Date 949331954 -3600
# Node ID 7d08b047b76e300bd159e5796f43f808a151de1d
# Parent  56d9baa2ddb022437f5393447f6938a99b8483c8
new theorem vimage_Union

diff -r 56d9baa2ddb0 -r 7d08b047b76e src/HOL/Vimage.ML
--- a/src/HOL/Vimage.ML	Mon Jan 31 16:18:42 2000 +0100
+++ b/src/HOL/Vimage.ML	Mon Jan 31 16:19:14 2000 +0100
@@ -41,7 +41,7 @@
 AddSEs [vimageE];
 
 
-(*** Simple equalities ***)
+(*** Equations ***)
 
 Goal "f-``{} = {}";
 by (Blast_tac 1);
@@ -59,6 +59,10 @@
 by (Fast_tac 1);
 qed "vimage_Int";
 
+Goal "f -`` (Union A) = (UN X:A. f -`` X)";
+by (Blast_tac 1);
+qed "vimage_Union";
+
 Goal "f-``(UN x:A. B x) = (UN x:A. f -`` B x)";
 by (Blast_tac 1);
 qed "vimage_UN";
@@ -92,9 +96,7 @@
 by (Blast_tac 1);
 qed "vimage_eq_UN";
 
-
-(** monotonicity **)
-
+(*monotonicity*)
 Goal "A<=B ==> f-``A <= f-``B";
 by (Blast_tac 1);
 qed "vimage_mono";