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