isabelle: src/ZF/AC/WO1_WO7.thy@746cd24ee3ac (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 ==
47d0d906b39a new file AC/WO1_WO7.thy paulson parents: diff changeset	15	ALL X. ~Finite(X) --> (EX R. well_ord(X,R) & ~well_ord(X,converse(R)))"
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	paulson
	Thu, 10 Sep 1998 17:49:36 +0200
changeset 5472	746cd24ee3ac
parent 5464	47d0d906b39a
child 11317	7f9e4c389318
permissions	-rw-r--r--