src/HOL/Isar_examples/document/root.bib

bib;

@string{CUCL="Comp. Lab., Univ. Camb."}
@string{CUP="Cambridge University Press"}
@string{Springer="Springer-Verlag"}
@string{TUM="TU Munich"}


@Book{davey-priestley,
  author	= {B. A. Davey and H. A. Priestley},
  title		= {Introduction to Lattices and Order},
  publisher	= CUP,
  year		= 1990}

@manual{isabelle-HOL,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {{Isabelle}'s Logics: {HOL}},
  institution	= {Institut f\"ur Informatik, Technische Universi\"at
                  M\"unchen and Computer Laboratory, University of Cambridge}}

@manual{isabelle-intro,
  author	= {Lawrence C. Paulson},
  title		= {Introduction to {Isabelle}},
  institution	= CUCL}

@manual{isabelle-isar-ref,
  author	= {Markus Wenzel},
  title		= {The {Isabelle Isar} Reference Manual},
  institution	= TUM}

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

@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 1690},
  year		= 1999}