src/ZF/Order.thy

--- a/src/ZF/Order.thy	Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/Order.thy	Fri Jan 03 15:01:55 1997 +0100
@@ -38,4 +38,9 @@
        UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s).   
             {<x,y>}"
 
+constdefs
+
+  first :: [i, i, i] => o
+    "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
+
 end