src/HOL/Lattice/document/root.bib

simplified a proof

@InProceedings{Bauer-Wenzel:2000:HB,
  author =       {Gertrud Bauer and Markus Wenzel},
  title =        {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
      {I}sabelle/{I}sar},
  booktitle =    {Types for Proofs and Programs: TYPES'99},
  editor =       {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
                  and Jan Smith},
  series =       {LNCS},
  year =         2000
}

@Book{Davey-Priestley:1990,
  author        = {B. A. Davey and H. A. Priestley},
  title         = {Introduction to Lattices and Order},
  publisher     = {Cambridge University Press},
  year          = 1990}

@InProceedings{Wenzel:1999:TPHOL,
  author =       {Markus Wenzel},
  title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
  crossref =     {tphols99}}


@Manual{Wenzel:2000:axclass,
  author        = {Markus Wenzel},
  title         = {Using Axiomatic Type Classes in Isabelle},
  year          = 2000,
  institution   = {TU Munich},
  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}
}

@Manual{Wenzel:2000:isar-ref,
  author        = {Markus Wenzel},
  title         = {The {Isabelle/Isar} Reference Manual},
  year          = 2000,
  institution   = {TU Munich},
  note          = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
}

@Proceedings{tphols99,
  title         = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
  booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
  editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
                  Paulin, C. and Thery, L.},
  series        = {LNCS},
  volume        = 1690,
  year          = 1999}