src/ZF/AC.thy
changeset 484 70b789956bd3
child 1478 2b8c2a7547ab
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC.thy	Tue Jul 26 13:21:20 1994 +0200
@@ -0,0 +1,14 @@
+(*  Title: 	ZF/AC.thy
+    ID:         $Id$
+    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.
+*)
+
+AC = ZF + "func" +
+rules
+  AC	"[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
+end