--- 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";