src/ZF/AC.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 14171 0cab06e3bbd0
--- 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*)