author | paulson |
Mon, 23 Sep 1996 18:18:18 +0200 | |
changeset 2010 | 0a22b9d63a18 |
parent 1478 | 2b8c2a7547ab |
child 2469 | b50b8c0eec01 |
permissions | -rw-r--r-- |
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 |
||
11 |
AC = ZF + "func" + |
|
12 |
rules |
|
1478 | 13 |
AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)" |
484 | 14 |
end |