author | lcp |
Tue, 29 Nov 1994 00:31:31 +0100 | |
changeset 753 | ec86863e87c8 |
parent 484 | 70b789956bd3 |
child 1478 | 2b8c2a7547ab |
permissions | -rw-r--r-- |
484 | 1 |
(* Title: ZF/AC.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
6 |
The Axiom of Choice |
|
7 |
||
8 |
This definition comes from Halmos (1960), page 59. |
|
9 |
*) |
|
10 |
||
11 |
AC = ZF + "func" + |
|
12 |
rules |
|
13 |
AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)" |
|
14 |
end |