# HG changeset patch
# User paulson
# Date 905441641 -7200
# Node ID 47d0d906b39a0c239b421f1952bb390ec01e1c19
# Parent  a5479f5cd4827bc48fa63689c4a765519d8dc98f
new file AC/WO1_WO7.thy

diff -r a5479f5cd482 -r 47d0d906b39a src/ZF/AC/WO1_WO7.thy
--- /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
diff -r a5479f5cd482 -r 47d0d906b39a src/ZF/IsaMakefile
--- 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