1
(* Title: ZF/AC/Hartog.thy
2
ID: $Id$
3
Author: Krzysztof Grabczewski
4
5
Hartog's function.
6
*)
7
8
Hartog = Cardinal +
9
10
consts
11
12
Hartog :: i => i
13
14
defs
15
16
Hartog_def "Hartog(X) == LEAST i. ~i lepoll X"
17
18
end