isabelle: src/ZF/AC.thy@adda1dc18bb8 (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 +
6053 8a1059aa01f0 new inductive, datatype and primrec packages, etc. paulson parents: 2469 diff changeset	12
8a1059aa01f0 new inductive, datatype and primrec packages, etc. paulson parents: 2469 diff changeset	13	constdefs
8a1059aa01f0 new inductive, datatype and primrec packages, etc. paulson parents: 2469 diff changeset	14	(Needs to be visible for Zorn.thy)
8a1059aa01f0 new inductive, datatype and primrec packages, etc. paulson parents: 2469 diff changeset	15	increasing :: i=>i
8a1059aa01f0 new inductive, datatype and primrec packages, etc. paulson parents: 2469 diff changeset	16	"increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
8a1059aa01f0 new inductive, datatype and primrec packages, etc. paulson parents: 2469 diff changeset	17
484 70b789956bd3 Axiom of choice, cardinality results, etc. lcp parents: diff changeset	18	rules
1478 2b8c2a7547ab expanded tabs clasohm parents: 484 diff changeset	19	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	20	end

author	wenzelm
	Sat, 02 Sep 2000 21:48:10 +0200
changeset 9802	adda1dc18bb8
parent 6053	8a1059aa01f0
child 13134	bf37a3049251
permissions	-rw-r--r--