Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/ZF.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2286 c2f76a5bad65 
--- a/src/ZF/ZF.thy	Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/ZF.thy	Tue Feb 06 12:27:17 1996 +0100
@@ -61,7 +61,7 @@
   range       :: i => i
   field       :: i => i
   converse    :: i => i
-  function    :: i => o	    	(*is a relation a function?*)
+  function    :: i => o         (*is a relation a function?*)
   Lambda      :: [i, i => i] => i
   restrict    :: [i, i] => i
 
@@ -214,8 +214,8 @@
   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')"
+  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"
isabelle