src/HOL/Relation.ML
changeset 5231 2a454140ae24
parent 5148 74919e8f221c
child 5316 7a8975451a89
     1.1 --- a/src/HOL/Relation.ML	Fri Jul 31 11:33:53 1998 +0200
     1.2 +++ b/src/HOL/Relation.ML	Fri Jul 31 18:46:28 1998 +0200
     1.3 @@ -242,3 +242,15 @@
     1.4  
     1.5  qed_goalw "UnivalentD" Relation.thy [Univalent_def] 
     1.6  	"!!r. [| Univalent r; (x,y):r; (x,z):r|] ==> y=z" (K [Auto_tac]);
     1.7 +
     1.8 +
     1.9 +(** Graphs of partial functions **)
    1.10 +
    1.11 +Goal "Domain{(x,y). y = f x & P x} = {x. P x}";
    1.12 +by (Blast_tac 1);
    1.13 +qed "Domain_partial_func";
    1.14 +
    1.15 +Goal "Range{(x,y). y = f x & P x} = f``{x. P x}";
    1.16 +by (Blast_tac 1);
    1.17 +qed "Range_partial_func";
    1.18 +