src/HOL/ex/document/root.bib

added section "Canonical reasoning patterns";
tuned;

@TechReport{Gordon:1985:HOL,
  author =       {M. J. C. Gordon},
  title =        {{HOL}: A machine oriented formulation of higher order logic},
  institution =  {University of Cambridge Computer Laboratory},
  year =         1985,
  number =       68
}

@inproceedings{HuttonW04,author={Graham Hutton and Joel Wright},
title={Compiling Exceptions Correctly},
booktitle={Proc.\ Conf.\ Mathematics of Program Construction},
year=2004,note={To appear}}

@InProceedings{Kamm-et-al:1999,
  author =       {Florian Kamm{\"u}ller and Markus Wenzel and
                  Lawrence C. Paulson},
  title =        {Locales: A Sectioning Concept for {Isabelle}},
  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}

@InProceedings{Naraschewski-Wenzel:1998,
  author        = {Wolfgang Naraschewski and Markus Wenzel},
  title         = {Object-Oriented Verification based on Record Subtyping in
                  {H}igher-{O}rder {L}ogic},
  booktitle     = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
  editor        = {Jim Grundy and Malcom Newey},
  series        = {LNCS},
  volume        = 1479,
  year          = 1998}

@Manual{Nipkow-et-al:2001:HOL,
  author        = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title         = {{Isabelle}'s Logics: {HOL}},
  institution   = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
                  M{\"u}nchen and Computer Laboratory, University of Cambridge},
  year          = 2001,
  note          = {Part of the Isabelle distribution,
                   \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}
}

@Article{Paulson:1989,
  author =       {L. C. Paulson},
  title =        {The foundation of a generic Theorem Prover},
  journal =      {Journal of Automated Reasoning},
  year =         1989,
  volume =       5,
  number =       3,
  pages =        {363--397}
}

@Book{Paulson:1994:Isabelle,
 author =        {L. C. Paulson and T. Nipkow},
  title =        {{Isabelle}: A Generic Theorem Prover},
  year =         1994,
  series =       {LNCS},
  volume =       {828},
  publisher =    {Springer}
}

@InProceedings{Wenzel:1999,
  author =       {Markus Wenzel},
  title =        {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
  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}

@Unpublished{Wenzel:2001:Isar-examples,
  author =       {Markus Wenzel},
  title =        {Miscellaneous {I}sabelle/{I}sar examples for
                  Higher-Order Logic},
  year =         2001,
  note =         {Part of the Isabelle distribution,
                  \url{http://isabelle.in.tum.de/library/HOL/Isar_examples/document.pdf}}
}

@PhdThesis{Wenzel:2001:Thesis,
  author = 	 {Markus Wenzel},
  title = 	 {Isabelle/Isar --- a versatile environment for human-readable
                  formal proof documents},
  school = 	 {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
  year = 	 2001,
  month =	 {September},
  note =	 {Submitted}
}
@Manual{Wenzel:2001:isar-ref,
  author        = {Markus Wenzel},
  title         = {The {Isabelle/Isar} Reference Manual},
  year          = 2001,
  institution   = {TU M{\"u}nchen},
  note          = {Part of the Isabelle distribution,
                   \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}
}

@Book{isabelle-hol-book,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  year		= 2002,
  note		= {LNCS 2283}}

@Misc{McMillan-LectureNotes,
  author =	 {Ken McMillan},
  title =	 {Lecture notes on verification of digital and hybrid systems},
  note =	 {{NATO} summer school, \url{http://www-cad.eecs.berkeley.edu/~kenmcmil/tutorial/toc.html}}
}

@PhdThesis{McMillan-PhDThesis,
  author = 	 {Ken McMillan},
  title = 	 {Symbolic Model Checking: an approach to the state explosion problem},
  school = 	 {Carnegie Mellon University},
  year = 	 1992
}