author  paulson 
Mon, 28 Dec 1998 16:59:28 +0100  
changeset 6053  8a1059aa01f0 
parent 2469  b50b8c0eec01 
child 13134  bf37a3049251 
permissions  rwrr 
1478  1 
(* Title: ZF/AC.thy 
484  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
484  4 
Copyright 1994 University of Cambridge 
5 

6 
The Axiom of Choice 

7 

8 
This definition comes from Halmos (1960), page 59. 

9 
*) 

10 

2469  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  18 
rules 
1478  19 
AC "[ a: A; !!x. x:A ==> (EX y. y:B(x)) ] ==> EX z. z : Pi(A,B)" 
484  20 
end 