src/ZF/ZF.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2286 c2f76a5bad65
     1.1 --- a/src/ZF/ZF.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/ZF.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4    range       :: i => i
     1.5    field       :: i => i
     1.6    converse    :: i => i
     1.7 -  function    :: i => o	    	(*is a relation a function?*)
     1.8 +  function    :: i => o         (*is a relation a function?*)
     1.9    Lambda      :: [i, i => i] => i
    1.10    restrict    :: [i, i] => i
    1.11  
    1.12 @@ -214,8 +214,8 @@
    1.13    domain_def    "domain(r) == {x. w:r, EX y. w=<x,y>}"
    1.14    range_def     "range(r) == domain(converse(r))"
    1.15    field_def     "field(r) == domain(r) Un range(r)"
    1.16 -  function_def	"function(r) == ALL x y. <x,y>:r -->   
    1.17 -		                (ALL y'. <x,y'>:r --> y=y')"
    1.18 +  function_def  "function(r) == ALL x y. <x,y>:r -->   
    1.19 +                                (ALL y'. <x,y'>:r --> y=y')"
    1.20    image_def     "r `` A  == {y : range(r) . EX x:A. <x,y> : r}"
    1.21    vimage_def    "r -`` A == converse(r)``A"
    1.22