doc-src/Locales/Locales/document/root.bib

Locales: new element constrains, parameter renaming with syntax,
experimental command instantiate withdrawn.

@phdthesis{Bailey1998,
  author = "Anthony Bailey",
  title = "The machine-checked literate formalisation of algebra in type theory",
  school = "University of Manchester",
  month = jan,
  year = 1998,
  available = { CB }
}

@phdthesis{Kammuller1999a,
  author = "Florian Kamm{\"u}ller",
  title = "Modular Reasoning in {Isabelle}",
  school = "University of Cambridge, Computer Laboratory",
  note = "Available as Technical Report No. 470.",
  month = aug,
  year = 1999,
  available = { CB }
}

% TYPES 98

@inproceedings{Kammuller1999b,
  author = "Florian Kamm{\"u}ller",
  title = "Modular Structures as Dependent Types in {Isabelle}",
  pages = "121--132",
  crossref = "AltenkirchEtAl1999",
  available = { CB }
}

@proceedings{AltenkirchEtAl1999,
  editor = "Thorsten Altenkirch and Wolfgang Naraschewski and Bernhard Reus",
  title = "Types for Proofs and Programs: International Workshop, {TYPES} '98, {Kloster Irsee, Germany, March 27--31, 1998}, Selected Papers",
  booktitle = "TYPES '98",
  publisher = "Springer",
  series = "LNCS 1657",
  year = 1999
}
% CADE-17

@inproceedings{Kammuller2000,
  author = "Florian Kamm{\"u}ller",
  title = "Modular Reasoning in {Isabelle}",
  pages = "99--114",
  crossref = "McAllester2000",
  available = { CB }
}

@proceedings{McAllester2000,
  editor = "David McAllester",
  title = "17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17--20, 2000: Proceedings",
  booktitle = "CADE 17",
  publisher = "Springer",
  series = "LNCS 1831",
  year = 2000
}

@book{NipkowEtAl2002,
  author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
  title = "{Isabelle/HOL}: A Proof Assistant for Higher-Order Logic",
  publisher = "Springer",
  series = "LNCS 2283",
  year = 2002,
  available = { CB }
}

% TYPES 2002

@inproceedings{Nipkow2003,
  author = "Tobias Nipkow",
  title = "Structured Proofs in {Isar/HOL}",
  pages = "259--278",
  crossref = "GeuversWiedijk2003"
}

@proceedings{GeuversWiedijk2003,
  editor = "H. Geuvers and F. Wiedijk",
  title = "Types for Proofs and Programs (TYPES 2002)",
  booktitle = "TYPES 2002",
  publisher = "Springer",
  series = "LNCS 2646",
  year = 2003
}

@phdthesis{Wenzel2002a,
  author = "Markus Wenzel",
  title = "{Isabelle/Isar} --- a versatile environment for human-readable formal proof documents",
  school = "Technische Universit{\"a}t M{\"u}nchen",
  note = "Electronically published as http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.",
  year = 2002
}

@unpublished{Wenzel2002b,
  author = "Markus Wenzel",
  title = "Using locales in {Isabelle/Isar}",
  note = "Part of the Isabelle2003 distribution, file src/HOL/ex/Locales.thy.  Distribution of Isabelle available at http://isabelle.in.tum.de",
  year = 2002
}

@unpublished{Wenzel2003,
  author = "Markus Wenzel",
  title = "The {Isabelle/Isar} Reference Manual",
  note = "Part of the Isabelle2003 distribution, available at http://isabelle.in.tum.de",
  year = 2003
}

% TPHOLs 2003

@inproceedings{Chrzaszcz2003,
  author = "Jacek Chrz{\c{a}}szcz",
  title = "Implementing Modules in the {Coq} System",
  pages = "270--286",
  crossref = "BasinWolff2003",
  available = { CB }
}

@proceedings{BasinWolff2003,
  editor = "David Basin and Burkhart Wolff",
  title = "Theorem proving in higher order logics: 16th International Conference, TPHOLs 2003, Rome, Italy, September 2003: proceedings",
  booktitle = "TPHOLs 2003",
  publisher = "Springer",
  series = "LNCS 2758",
  year = 2003
}

@PhdThesis{Klein2003,
  author = "Gerwin Klein",
  title = "Verified Java Bytecode Verification",
  school = "Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen",
  year = 2003
}

% TACAS 2000

@inproceedings{Aspinall2000,
  author = "David Aspinall",
  title = "Proof General: A Generic Tool for Proof Development",
  pages = "38--42",
  crossref = "GrafSchwartzbach2000"
}

@proceedings{GrafSchwartzbach2000,
  editor    = {Susanne Graf and Michael I. Schwartzbach},
  title     = {Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 -- April 2, 2000, Proceedings},
  booktitle     = "TACAS 2000",
  publisher = {Springer},
  series    = {LNCS 1785},
  year      = {2000},
}

% TYPES 2004

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

@inproceedings{Chrzaszcz2004,
  author = "Jacek Chrz{\c{a}}szcz",
  title = "Modules in {Coq} Are and Will Be Correct",
  pages = "130--136",
  crossref = "BerardiEtAl2004",
  available = { CB }
}
@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
}