| changeset 6005 | 45186ec4d8b6 |
| parent 5998 | b2ecd577b8a3 |
| child 6806 | 43c081a0858d |
--- 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 ***)