src/ZF/Order.thy
changeset 2469 b50b8c0eec01
parent 1851 7b1e1c298e50
child 9683 f87c8c449018
     1.1 --- a/src/ZF/Order.thy	Fri Jan 03 10:48:28 1997 +0100
     1.2 +++ b/src/ZF/Order.thy	Fri Jan 03 15:01:55 1997 +0100
     1.3 @@ -38,4 +38,9 @@
     1.4         UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).   
     1.5              {<x,y>}"
     1.6  
     1.7 +constdefs
     1.8 +
     1.9 +  first :: [i, i, i] => o
    1.10 +    "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
    1.11 +
    1.12  end