author | clasohm |
Fri, 17 Nov 1995 13:22:50 +0100 | |
changeset 1341 | 69fec018854c |
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 |