src/ZF/AC/WO1_WO7.thy

--- a/src/ZF/AC/WO1_WO7.thy	Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/AC/WO1_WO7.thy	Sun Oct 07 21:19:31 2007 +0200
@@ -11,8 +11,7 @@
 
 theory WO1_WO7 imports AC_Equiv begin
 
-constdefs
-  LEMMA :: o
+definition
     "LEMMA ==
      \<forall>X. ~Finite(X) --> (\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))"