equal
deleted
inserted
replaced
1 (* Title: ZF/AC.thy |
1 (* Title: ZF/AC.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 The Axiom of Choice |
6 The Axiom of Choice |
7 |
7 |
8 This definition comes from Halmos (1960), page 59. |
8 This definition comes from Halmos (1960), page 59. |
9 *) |
9 *) |
10 |
10 |
11 AC = ZF + "func" + |
11 AC = ZF + "func" + |
12 rules |
12 rules |
13 AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)" |
13 AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)" |
14 end |
14 end |