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