--- a/src/ZF/AC.thy Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/AC.thy Tue Jul 09 23:05:26 2002 +0200
@@ -3,13 +3,13 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-The Axiom of Choice
+*)
-This definition comes from Halmos (1960), page 59.
-*)
+header{*The Axiom of Choice*}
theory AC = Main:
+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)"
(*The same as AC, but no premise a \<in> A*)