src/HOL/Relation.ML
changeset 6005 45186ec4d8b6
parent 5998 b2ecd577b8a3
child 6806 43c081a0858d
     1.1 --- a/src/HOL/Relation.ML	Tue Dec 01 14:48:24 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Wed Dec 02 15:52:39 1998 +0100
     1.3 @@ -206,6 +206,10 @@
     1.4  by (Blast_tac 1);
     1.5  qed "Domain_Diff_subset";
     1.6  
     1.7 +Goal "Domain (Union S) = (UN A:S. Domain A)";
     1.8 +by (Blast_tac 1);
     1.9 +qed "Domain_Union";
    1.10 +
    1.11  
    1.12  (** Range **)
    1.13  
    1.14 @@ -248,6 +252,10 @@
    1.15  by (Blast_tac 1);
    1.16  qed "Range_Diff_subset";
    1.17  
    1.18 +Goal "Range (Union S) = (UN A:S. Range A)";
    1.19 +by (Blast_tac 1);
    1.20 +qed "Range_Union";
    1.21 +
    1.22  
    1.23  (*** Image of a set under a relation ***)
    1.24