src/HOL/document/root.bib

sorted out cases in negligible_standard_hyperplane

@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}
}