src/HOL/document/root.bib

insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem

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