@book{card-book,
title = {Introduction to {C}ardinal {A}rithmetic},
author = {M. Holz and K. Steffens and E. Weitz},
publisher = "Birkh{\"{a}}user",
year = 1999,
}
@Book{davenport92,
author = {H. Davenport},
title = {The Higher Arithmetic},
publisher = {Cambridge University Press},
year = 1992
}
@InProceedings{paulin-tlca,
author = {Christine Paulin-Mohring},
title = {Inductive Definitions in the System {Coq}: Rules and
Properties},
crossref = {tlca93},
pages = {328-345}}
@Proceedings{tlca93,
title = {Typed Lambda Calculi and Applications},
booktitle = {Typed Lambda Calculi and Applications},
editor = {M. Bezem and J.F. Groote},
year = 1993,
publisher = {Springer},
series = {LNCS 664}}
@book{Birkhoff79,
author = {Garret Birkhoff},
title = {Lattice Theory},
publisher = {American Mathematical Society},
year=1979
}
@book{Nipkow-et-al:2002:tutorial,
author = {T. Nipkow and L. C. Paulson and M. Wenzel},
title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
series = {LNCS},
volume = 2283,
year = 2002,
publisher = {Springer-Verlag}
}