doc-src/Locales/document/root.bib

more standard document preparation within session context;

@unpublished{IsarRef,
  author = "Markus Wenzel",
  title = "The {Isabelle/Isar} Reference Manual",
  note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}."
}

@book {Jacobson1985,
  author = "Nathan Jacobson",
  title = "Basic Algebra",
  volume = "I",
  publisher = "Freeman",
  edition = "2nd",
  year = 1985,
  available = { CB }
}

% TYPES 2006

@inproceedings{HaftmannWenzel2007,
  author = "Florian Haftmann and Makarius Wenzel",
  title = "Constructive Type Classes in {Isabelle}",
  pages = "160--174",
  crossref = "AltenkirchMcBride2007",
  available = { CB }
}

@proceedings{AltenkirchMcBride2007,
  editor = "Thorsten Altenkirch and Connor McBride",
  title = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
  booktitle = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
  publisher = "Springer",
  series = "LNCS 4502",
  year = 2007
}


@techreport{Ballarin2006a,
  author = "Clemens Ballarin",
  title = "Interpretation of Locales in {Isabelle}: Managing Dependencies between Locales",
  institution = "Technische Universit{\"a}t M{\"u}nchen",
  number = "TUM-I0607",
  year = 2006
}

% TYPES 2003

@inproceedings{Ballarin2004a,
  author = "Clemens Ballarin",
  title = "Locales and Locale Expressions in {Isabelle/Isar}",
  pages = "34--50",
  crossref = "BerardiEtAl2004"
}

@proceedings{BerardiEtAl2004,
  editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
  title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
  booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
  publisher = "Springer",
  series = "LNCS 3085",
  year = 2004
}

% TYPES 2008

@inproceedings{HaftmannWenzel2009,
  author = "Florian Haftmann and Makarius Wenzel",
  title = "Local theory specifications in {Isabelle}/{Isar}",
  pages = "153--168",
  crossref = "BerardiEtAl2009"
}

@proceedings{BerardiEtAl2009,
  editor = "Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro",
  title = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
  booktitle = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
  series = "LNCS 5497",
  publisher = "Springer",
  year = 2009
}

% MKM 2006

@inproceedings{Ballarin2006b,
  author = "Clemens Ballarin",
  title = "Interpretation of Locales in {Isabelle}: Theories and Proof Contexts",
  pages = "31--43",
  crossref = "BorweinFarmer2006"
}

@proceedings{BorweinFarmer2006,
  editor = "Jonathan M. Borwein and William M. Farmer",
  title = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
  booktitle = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
  series = "LNCS 4108",
  publisher = "Springer",
  year = 2006,
  available = { CB }
}

% TPHOLs 1999

@inproceedings{KammullerEtAl1999,
  author = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson",
  title = "Locales: A Sectioning Concept for {Isabelle}",
  pages = "149--165",
  crossref = "BertotEtAl1999",
  available = { CB }
}

@book{BertotEtAl1999,
  editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry",
  title = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
  booktitle = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
  publisher = "Springer",
  series = "LNCS 1690",
  year = 1999
}