# HG changeset patch
# User paulson
# Date 1020845704 -7200
# Node ID 4888694b2829a52152ffba7d8d9c65270587cbc3
# Parent  d1fea11b2fb680cd3682db3a52442df90035be1e
the new predicate "relation"

diff -r d1fea11b2fb6 -r 4888694b2829 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed May 08 10:14:35 2002 +0200
+++ b/src/ZF/ZF.thy	Wed May 08 10:15:04 2002 +0200
@@ -71,7 +71,8 @@
   range       :: i => i
   field       :: i => i
   converse    :: i => i
-  function    :: i => o         (*is a relation a function?*)
+  relation    :: i => o         (*recognizes sets of pairs*)
+  function    :: i => o         (*recognizes functions; can have non-pairs*)
   Lambda      :: [i, i => i] => i
   restrict    :: [i, i] => i
 
@@ -251,8 +252,9 @@
   domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
   range_def     "range(r) == domain(converse(r))"
   field_def     "field(r) == domain(r) Un range(r)"
-  function_def  "function(r) == ALL x y. <x,y>:r -->
-                                (ALL y'. <x,y'>:r --> y=y')"
+  relation_def  "relation(r) == ALL z:r. EX x y. z = <x,y>"
+  function_def  "function(r) ==
+		    ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y')"
   image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
   vimage_def    "r -`` A == converse(r)``A"