# HG changeset patch
# User paulson
# Date 961576294 -7200
# Node ID 44cd0f9f8e5b0cff2c2b16f943362ba0dbcb3a29
# Parent  5c4d4364f854540b2900fade8abbebadf74f92d9
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split

diff -r 5c4d4364f854 -r 44cd0f9f8e5b src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Wed Jun 21 10:30:36 2000 +0200
+++ b/src/HOL/Relation.ML	Wed Jun 21 10:31:34 2000 +0200
@@ -411,16 +411,21 @@
 qed "univalentD";
 
 
-(** Graphs of partial functions **)
+(** Graphs given by Collect **)
+
+Goal "Domain{(x,y). P x y} = {x. EX y. P x y}";
+by Auto_tac; 
+qed "Domain_Collect_split";
 
-Goal "Domain{(x,y). y = f x & P x} = {x. P x}";
-by (Blast_tac 1);
-qed "Domain_partial_func";
+Goal "Range{(x,y). P x y} = {y. EX x. P x y}";
+by Auto_tac; 
+qed "Range_Collect_split";
 
-Goal "Range{(x,y). y = f x & P x} = f``{x. P x}";
-by (Blast_tac 1);
-qed "Range_partial_func";
+Goal "{(x,y). P x y} ^^ A = {y. EX x:A. P x y}";
+by Auto_tac; 
+qed "Image_Collect_split";
 
+Addsimps [Domain_Collect_split, Range_Collect_split, Image_Collect_split];
 
 (** Composition of function and relation **)