# HG changeset patch
# User paulson
# Date 901903588 -7200
# Node ID 2a454140ae2414ed168134b52864a6b33239868e
# Parent  fdc28193ccf7ae515c32da5c043b3431e19260de
new theorems for partial funcs

diff -r fdc28193ccf7 -r 2a454140ae24 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Fri Jul 31 11:33:53 1998 +0200
+++ b/src/HOL/Relation.ML	Fri Jul 31 18:46:28 1998 +0200
@@ -242,3 +242,15 @@
 
 qed_goalw "UnivalentD" Relation.thy [Univalent_def] 
 	"!!r. [| Univalent r; (x,y):r; (x,z):r|] ==> y=z" (K [Auto_tac]);
+
+
+(** Graphs of partial functions **)
+
+Goal "Domain{(x,y). y = f x & P x} = {x. P x}";
+by (Blast_tac 1);
+qed "Domain_partial_func";
+
+Goal "Range{(x,y). y = f x & P x} = f``{x. P x}";
+by (Blast_tac 1);
+qed "Range_partial_func";
+