doc-src/IsarOverview/Isar/document/root.bib

prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);

@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
@string{Springer="Springer-Verlag"}
@string{JAR="J. Automated Reasoning"}

@InProceedings{BauerW-TPHOLs01,
author={Gertrud Bauer and Markus Wenzel},
title={Calculational Reasoning Revisited --- an {Isabelle/Isar} Experience},
booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001},
editor={R. Boulton and P. Jackson},
year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"}

@book{LCF,author="M.C.J. Gordon and Robin Milner and C.P. Wadsworth",
title="Edinburgh {LCF}: a Mechanised Logic of Computation",
publisher=Springer,series=LNCS,volume=78,year=1979}

@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher=Springer,series=LNCS,volume=2283,year=2002,
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}

@article{KleinN-TOPLAS,author={Gerwin Klein and Tobias Nipkow},
title={A Machine-Checked Model for a {Java}-Like Language, Virtual Machine and Compiler},
journal=TOPLAS,volume = {28}, number = {4}, year = {2006}, pages = {619--695},
doi = {http://doi.acm.org/10.1145/1146809.1146811}}

@InProceedings{Rudnicki92,author={P. Rudnicki},
title={An Overview of the {Mizar} Project},
booktitle={Workshop on Types for Proofs and Programs},
year=1992,organization={Chalmers University of Technology}}

@manual{Isar-Ref-Man,author="Markus Wenzel",
title="The Isabelle/Isar Reference Manual",
organization={Technische Universit{\"a}t M{\"u}nchen},year=2002,
note={\url{http://isabelle.in.tum.de/dist/Isabelle2002/doc/isar-ref.pdf}}}

@article{WenzelW-JAR,author={Markus Wenzel and Freek Wiedijk},
title={A comparison of the mathematical proof languages {Mizar} and {Isar}},
journal=JAR,year=2002,pages={389--411}}