isabelle: src/ZF/AC.thy@6f71b5d46700 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 484 diff changeset	1	(* Title: ZF/AC.thy
484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 484 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	4	Copyright 1994 University of Cambridge
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	5
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	6	The Axiom of Choice
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	7
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	8	This definition comes from Halmos (1960), page 59.
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	9	*)
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	10
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	11	AC = ZF + "func" +
70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	12	rules
1478 2b8c2a7547ab expanded tabs clasohm parents: 484 diff changeset	13	AC "[\| a: A; !!x. x:A ==> (EX y. y:B(x)) \|] ==> EX z. z : Pi(A,B)"
484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	14	end

author	paulson
	Wed, 06 Mar 1996 12:52:11 +0100
changeset 1552	6f71b5d46700
parent 1478	2b8c2a7547ab
child 2469	b50b8c0eec01
permissions	-rw-r--r--