--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/WO1_WO7.thy Thu Sep 10 17:34:01 1998 +0200
@@ -0,0 +1,17 @@
+(* Title: ZF/AC/WO1_WO7.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, CU Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5)
+LEMMA is the sentence denoted by (**)
+*)
+
+WO1_WO7 = AC_Equiv +
+
+constdefs
+ LEMMA :: o
+ "LEMMA ==
+ ALL X. ~Finite(X) --> (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))"
+
+end
--- a/src/ZF/IsaMakefile Thu Sep 10 17:33:09 1998 +0200
+++ b/src/ZF/IsaMakefile Thu Sep 10 17:34:01 1998 +0200
@@ -80,7 +80,7 @@
AC/AC_Equiv.thy AC/Cardinal_aux.ML AC/Cardinal_aux.thy AC/DC.ML \
AC/DC.thy AC/DC_lemmas.ML AC/DC_lemmas.thy AC/HH.ML AC/HH.thy \
AC/Hartog.ML AC/Hartog.thy AC/ROOT.ML AC/WO1_AC.ML AC/WO1_AC.thy \
- AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO8.ML AC/WO2_AC16.ML \
+ AC/WO1_WO6.ML AC/WO1_WO7.ML AC/WO1_WO7.thy AC/WO1_WO8.ML AC/WO2_AC16.ML \
AC/WO2_AC16.thy AC/WO6_WO1.ML AC/WO6_WO1.thy AC/WO_AC.ML AC/WO_AC.thy \
AC/recfunAC16.ML AC/recfunAC16.thy AC/rel_is_fun.ML AC/rel_is_fun.thy
@$(ISATOOL) usedir $(OUT)/ZF AC