src/ZF/AC.thy
author paulson
Mon Dec 28 16:59:28 1998 +0100 (1998-12-28)
changeset 6053 8a1059aa01f0
parent 2469 b50b8c0eec01
child 13134 bf37a3049251
permissions -rw-r--r--
new inductive, datatype and primrec packages, etc.
clasohm@1478
     1
(*  Title:      ZF/AC.thy
lcp@484
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@484
     4
    Copyright   1994  University of Cambridge
lcp@484
     5
lcp@484
     6
The Axiom of Choice
lcp@484
     7
lcp@484
     8
This definition comes from Halmos (1960), page 59.
lcp@484
     9
*)
lcp@484
    10
paulson@2469
    11
AC = func +
paulson@6053
    12
paulson@6053
    13
constdefs
paulson@6053
    14
  (*Needs to be visible for Zorn.thy*)
paulson@6053
    15
  increasing :: i=>i
paulson@6053
    16
    "increasing(A) == {f: Pow(A)->Pow(A). ALL x. x<=A --> x<=f`x}"
paulson@6053
    17
lcp@484
    18
rules
clasohm@1478
    19
  AC    "[| a: A;  !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"
lcp@484
    20
end