isabelle: src/ZF/AC/WO1_WO7.thy@1a386a1e002c (annotated)

5464 47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	1	(* Title: ZF/AC/WO1_WO7.thy
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	2	ID: $Id$
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	3	Author: Lawrence C Paulson, CU Computer Laboratory
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	5
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	6	WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5)
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	7	LEMMA is the sentence denoted by (**)
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	8	*)
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	9
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	10	WO1_WO7 = AC_Equiv +
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	11
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	12	constdefs
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	13	LEMMA :: o
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	14	"LEMMA ==
11317 7f9e4c389318 X-symbols for set theory paulson parents: 5464 diff changeset	15	\\<forall>X. ~Finite(X) --> (\\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))"
5464 47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	16
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	17	end

author	wenzelm
	Mon, 22 Oct 2001 17:58:11 +0200
changeset 11879	1a386a1e002c
parent 11317	7f9e4c389318
child 12776	249600a63ba9
permissions	-rw-r--r--