src/ZF/AC/Hartog.thy

Introduction of integer division algorithm

Renaming of theorems from _nat0 to _int0 and _nat1 to _int1

(*  Title:      ZF/AC/Hartog.thy
    ID:         $Id$
    Author:     Krzysztof Grabczewski

Hartog's function.
*)

Hartog = Cardinal +

consts

  Hartog :: i => i

defs

  Hartog_def "Hartog(X) == LEAST i. ~i lepoll X"

end