src/ZF/AC.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 484 70b789956bd3
child 2469 b50b8c0eec01
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/AC.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 The Axiom of Choice
     7 
     8 This definition comes from Halmos (1960), page 59.
     9 *)
    10 
    11 AC = ZF + "func" +
    12 rules
    13   AC    "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
    14 end