isabelle: src/ZF/AC.thy@60205b0de9b9 (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
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1478 diff changeset	11	AC = func +
484 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
	Mon, 13 Jul 1998 16:43:57 +0200
changeset 5137	60205b0de9b9
parent 2469	b50b8c0eec01
child 6053	8a1059aa01f0
permissions	-rw-r--r--