--- a/src/ZF/ZF.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/ZF.thy Thu Jun 22 17:13:05 1995 +0200
@@ -159,8 +159,8 @@
foundation "A=0 | (EX x:A. ALL y:x. y~:A)"
(*Schema axiom since predicate P is a higher-order variable*)
- replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> \
- \ b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
+ replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==>
+ b : PrimReplace(A,P) <-> (EX x:A. P(x,b))"
defs
@@ -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"