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

}

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

}