new theorems Domain_Union, Range_Union

--- a/src/HOL/Relation.ML	Tue Dec 01 14:48:24 1998 +0100
+++ b/src/HOL/Relation.ML	Wed Dec 02 15:52:39 1998 +0100
@@ -206,6 +206,10 @@
 by (Blast_tac 1);
 qed "Domain_Diff_subset";
 
+Goal "Domain (Union S) = (UN A:S. Domain A)";
+by (Blast_tac 1);
+qed "Domain_Union";
+
 
 (** Range **)
 
@@ -248,6 +252,10 @@
 by (Blast_tac 1);
 qed "Range_Diff_subset";
 
+Goal "Range (Union S) = (UN A:S. Range A)";
+by (Blast_tac 1);
+qed "Range_Union";
+
 
 (*** Image of a set under a relation ***)