src/ZF/AC/first.thy

--- a/src/ZF/AC/first.thy	Tue Jul 25 17:03:59 1995 +0200
+++ b/src/ZF/AC/first.thy	Tue Jul 25 17:31:53 1995 +0200
@@ -10,14 +10,10 @@
 consts
 
   first                   :: "[i, i, i] => o"
-  exists_first            :: "[i, i] => o"
 
 defs
 
-  first_def                "first(u, X, R)
- 			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"
-
-  exists_first_def         "exists_first(X,R)
- 			    == EX u:X. first(u, X, R)"
+  first_def                "first(u, X, R) 
+			    == u:X & (ALL v:X. v~=u --> <u,v> : R)"
 
 end
\ No newline at end of file