@string{CUCL="Comp. Lab., Univ. Camb."}

@string{CUP="Cambridge University Press"}

@string{Springer="Springer-Verlag"}

@string{TUM="TU Munich"}

@Book{Concrete-Math,

  author = 	 {R. L. Graham and D. E. Knuth and O. Patashnik},

  title = 	 {Concrete Mathematics},

  publisher = 	 {Addison-Wesley},

  year = 	 1989

}

@InProceedings{Naraschewski-Wenzel:1998:HOOL,

  author	= {Wolfgang Naraschewski and Markus Wenzel},

  title		= {Object-Oriented Verification based on Record Subtyping in

                  {H}igher-{O}rder {L}ogic},

  crossref      = {tphols98}}

@Article{Nipkow:1998:Winskel,

  author = 	 {Tobias Nipkow},

  title = 	 {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},

  journal = 	 {Formal Aspects of Computing},

  year = 	 1998,

  volume =	 10,

  pages =	 {171--186}

}

@InProceedings{Wenzel:1999:TPHOL,

  author = 	 {Markus Wenzel},

  title = 	 {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},

  crossref =     {tphols99}}

@Book{Winskel:1993,

  author = 	 {G. Winskel},

  title = 	 {The Formal Semantics of Programming Languages},

  publisher = 	 {MIT Press},

  year = 	 1993

}

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

@manual{isabelle-ref,

  author	= {Lawrence C. Paulson},

  title		= {The {Isabelle} Reference Manual},

  institution	= CUCL}

@TechReport{paulson-mutilated-board,

  author = 	 {Lawrence C. Paulson},

  title = 	 {A Simple Formalization and Proof for the Mutilated Chess Board},

  institution =  CUCL,

  year = 	 1996,

  number =	 394,

  note = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Reports/mutil.pdf}}

}

@Proceedings{tphols98,

  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},

  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '98},

  editor	= {Jim Grundy and Malcom Newey},

  series	= {LNCS},

  volume        = 1479,

  year		= 1998}

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