src/ZF/OrderArith.thy
 changeset 1155 928a16e02f9f parent 753 ec86863e87c8 child 1401 0c439768f45c
```     1.1 --- a/src/ZF/OrderArith.thy	Thu Jun 22 12:58:39 1995 +0200
1.2 +++ b/src/ZF/OrderArith.thy	Thu Jun 22 17:13:05 1995 +0200
1.3 @@ -13,17 +13,17 @@
1.4
1.5  defs
1.6    (*disjoint sum of two relations; underlies ordinal addition*)
1.8 -\                {z: (A+B) * (A+B).  \
1.9 -\                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 \
1.10 -\                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 \
1.11 -\                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
1.13 +                {z: (A+B) * (A+B).
1.14 +                    (EX x y. z = <Inl(x), Inr(y)>)   |
1.15 +                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |
1.16 +                    (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
1.17
1.18    (*lexicographic product of two relations; underlies ordinal multiplication*)
1.19 -  rmult_def "rmult(A,r,B,s) == \
1.20 -\                {z: (A*B) * (A*B).  \
1.21 -\                    EX x' y' x y. z = <<x',y'>, <x,y>> &	 \
1.22 -\                       (<x',x>: r | (x'=x & <y',y>: s))}"
1.23 +  rmult_def "rmult(A,r,B,s) ==
1.24 +                {z: (A*B) * (A*B).
1.25 +                    EX x' y' x y. z = <<x',y'>, <x,y>> &
1.26 +                       (<x',x>: r | (x'=x & <y',y>: s))}"
1.27
1.28    (*inverse image of a relation*)
1.29    rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
```