| changeset 16417 | 9bc16273c2d4 |
| parent 14171 | 0cab06e3bbd0 |
| child 24893 | b8ef7afe3a6b |
--- a/src/ZF/AC.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/ZF/AC.thy Fri Jun 17 16:12:49 2005 +0200 @@ -7,7 +7,7 @@ header{*The Axiom of Choice*} -theory AC = Main: +theory AC imports Main begin text{*This definition comes from Halmos (1960), page 59.*} axioms AC: "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"