src/ZF/OrderArith.thy
 changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 9883 c1c8647af477
```--- a/src/ZF/OrderArith.thy	Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/OrderArith.thy	Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/OrderArith.thy
+(*  Title:      ZF/OrderArith.thy
ID:         \$Id\$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright   1994  University of Cambridge

Towards ordinal arithmetic
@@ -15,14 +15,14 @@
(*disjoint sum of two relations; underlies ordinal addition*)
{z: (A+B) * (A+B).
-                    (EX x y. z = <Inl(x), Inr(y)>)   |
-                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |
+                    (EX x y. z = <Inl(x), Inr(y)>)   |
+                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |
(EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"

(*lexicographic product of two relations; underlies ordinal multiplication*)
rmult_def "rmult(A,r,B,s) ==
{z: (A*B) * (A*B).
-                    EX x' y' x y. z = <<x',y'>, <x,y>> &
+                    EX x' y' x y. z = <<x',y'>, <x,y>> &
(<x',x>: r | (x'=x & <y',y>: s))}"

(*inverse image of a relation*)```