src/HOL/document/root.bib

clarified names to emphasize suble differences in meaning;

@book{Birkhoff79,
  author =      {Garret Birkhoff},
  title =       {Lattice Theory},
  publisher =   {American Mathematical Society},
  year=1979
}

@Book{davenport92,
  author =	 {H. Davenport},
  title = 	 {The Higher Arithmetic},
  publisher = 	 {Cambridge University Press},
  year = 	 1992
}

@book{GKP_CM,
 author = {Graham, Ronald L. and Knuth, Donald E. and Patashnik, Oren},
 title = {Concrete Mathematics: A Foundation for Computer Science},
 year = {1994},
 isbn = {0201558025},
 edition = {2nd},
 publisher = {Addison--Wesley},
 address = {Boston, MA, USA},
}

@techreport{Gordon-TR68,
  author = "Mike Gordon",
  title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",
  institution = "University of Cambridge, Computer Laboratory",
  number = 68,
  year = 1985
}

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

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