author | paulson |
Mon, 21 May 2001 14:45:52 +0200 | |
changeset 11317 | 7f9e4c389318 |
parent 5464 | 47d0d906b39a |
child 12776 | 249600a63ba9 |
permissions | -rw-r--r-- |
(* 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 == \\<forall>X. ~Finite(X) --> (\\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))" end