@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
}