src/ZF/Order.thy
changeset 578 efc648d29dd0
parent 435 ca5356bd315a
child 786 2a871417e7fc
     1.1 --- a/src/ZF/Order.thy	Thu Aug 25 10:41:17 1994 +0200
     1.2 +++ b/src/ZF/Order.thy	Thu Aug 25 12:09:21 1994 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    ord_iso         :: "[i,i,i,i]=>i"	(*Order isomorphisms*)
     1.5    pred            :: "[i,i,i]=>i"	(*Set of predecessors*)
     1.6  
     1.7 -rules
     1.8 +defs
     1.9    part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
    1.10  
    1.11    linear_def   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"