--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Locales/document/root.bib Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,117 @@
+@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
+}