# HG changeset patch # User paulson # Date 912610359 -3600 # Node ID 45186ec4d8b6587e3cc037adfe4f1addf343f65e # Parent 47705248cf80550509a6dbe39a128e4c2d61ddb9 new theorems Domain_Union, Range_Union diff -r 47705248cf80 -r 45186ec4d8b6 src/HOL/Relation.ML --- 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 ***)