src/ZF/AC/Hartog.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 12776 249600a63ba9
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      ZF/AC/Hartog.thy
lcp@1123
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Krzysztof Grabczewski
lcp@1123
     4
lcp@1123
     5
Hartog's function.
lcp@1123
     6
*)
lcp@1123
     7
lcp@1123
     8
Hartog = Cardinal +
lcp@1123
     9
lcp@1123
    10
consts
lcp@1123
    11
clasohm@1401
    12
  Hartog :: i => i
lcp@1123
    13
lcp@1123
    14
defs
lcp@1123
    15
lcp@1123
    16
  Hartog_def "Hartog(X) == LEAST i. ~i lepoll X"
lcp@1123
    17
lcp@1203
    18
end