src/ZF/OrderArith.thy
changeset 753 ec86863e87c8
parent 437 435875e4b21d
child 1155 928a16e02f9f
     1.1 --- a/src/ZF/OrderArith.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/OrderArith.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    radd, rmult      :: "[i,i,i,i]=>i"
     1.5    rvimage          :: "[i,i,i]=>i"
     1.6  
     1.7 -rules
     1.8 +defs
     1.9    (*disjoint sum of two relations; underlies ordinal addition*)
    1.10    radd_def "radd(A,r,B,s) == \
    1.11  \                {z: (A+B) * (A+B).  \