src/ZF/OrderArith.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 9883 c1c8647af477
     1.1 --- a/src/ZF/OrderArith.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/OrderArith.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/OrderArith.thy
     1.5 +(*  Title:      ZF/OrderArith.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1994  University of Cambridge
    1.10  
    1.11  Towards ordinal arithmetic 
    1.12 @@ -15,14 +15,14 @@
    1.13    (*disjoint sum of two relations; underlies ordinal addition*)
    1.14    radd_def "radd(A,r,B,s) == 
    1.15                  {z: (A+B) * (A+B).  
    1.16 -                    (EX x y. z = <Inl(x), Inr(y)>)   | 	 
    1.17 -                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   | 	 
    1.18 +                    (EX x y. z = <Inl(x), Inr(y)>)   |   
    1.19 +                    (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |      
    1.20                      (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
    1.21  
    1.22    (*lexicographic product of two relations; underlies ordinal multiplication*)
    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 +                    EX x' y' x y. z = <<x',y'>, <x,y>> &         
    1.27                         (<x',x>: r | (x'=x & <y',y>: s))}"
    1.28  
    1.29    (*inverse image of a relation*)