src/Doc/Locales/document/root.bib
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 48985 5386df44a037
child 68649 f849fc1cb65e
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     1
@unpublished{IsarRef,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     2
  author = "Markus Wenzel",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     3
  title = "The {Isabelle/Isar} Reference Manual",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     4
  note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}."
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     5
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
     6
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     7
@book {Jacobson1985,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     8
  author = "Nathan Jacobson",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
     9
  title = "Basic Algebra",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    10
  volume = "I",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    11
  publisher = "Freeman",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    12
  edition = "2nd",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    13
  year = 1985,
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    14
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    15
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    16
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    17
% TYPES 2006
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    18
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    19
@inproceedings{HaftmannWenzel2007,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    20
  author = "Florian Haftmann and Makarius Wenzel",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    21
  title = "Constructive Type Classes in {Isabelle}",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    22
  pages = "160--174",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    23
  crossref = "AltenkirchMcBride2007",
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    24
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    25
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    26
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    27
@proceedings{AltenkirchMcBride2007,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    28
  editor = "Thorsten Altenkirch and Connor McBride",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    29
  title = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    30
  booktitle = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    31
  publisher = "Springer",
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    32
  series = "LNCS 4502",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    33
  year = 2007
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    34
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    35
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    36
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    37
@techreport{Ballarin2006a,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    38
  author = "Clemens Ballarin",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    39
  title = "Interpretation of Locales in {Isabelle}: Managing Dependencies between Locales",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    40
  institution = "Technische Universit{\"a}t M{\"u}nchen",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    41
  number = "TUM-I0607",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    42
  year = 2006
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    43
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    44
32983
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    45
% TYPES 2003
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    46
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    47
@inproceedings{Ballarin2004a,
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    48
  author = "Clemens Ballarin",
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    49
  title = "Locales and Locale Expressions in {Isabelle/Isar}",
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    50
  pages = "34--50",
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    51
  crossref = "BerardiEtAl2004"
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    52
}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    53
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    54
@proceedings{BerardiEtAl2004,
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    55
  editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    56
  title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    57
  booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    58
  publisher = "Springer",
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    59
  series = "LNCS 3085",
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    60
  year = 2004
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    61
}
a6914429005b Finished revisions of locales tutorial.
ballarin
parents: 32981
diff changeset
    62
32981
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    63
% TYPES 2008
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    64
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    65
@inproceedings{HaftmannWenzel2009,
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    66
  author = "Florian Haftmann and Makarius Wenzel",
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    67
  title = "Local theory specifications in {Isabelle}/{Isar}",
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    68
  pages = "153--168",
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    69
  crossref = "BerardiEtAl2009"
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    70
}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    71
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    72
@proceedings{BerardiEtAl2009,
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    73
  editor = "Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro",
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    74
  title = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    75
  booktitle = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    76
  series = "LNCS 5497",
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    77
  publisher = "Springer",
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    78
  year = 2009
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    79
}
0114e04a0d64 Save current state of locales tutorial.
ballarin
parents: 27063
diff changeset
    80
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    81
% MKM 2006
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    82
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    83
@inproceedings{Ballarin2006b,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    84
  author = "Clemens Ballarin",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    85
  title = "Interpretation of Locales in {Isabelle}: Theories and Proof Contexts",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    86
  pages = "31--43",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    87
  crossref = "BorweinFarmer2006"
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    88
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    89
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    90
@proceedings{BorweinFarmer2006,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    91
  editor = "Jonathan M. Borwein and William M. Farmer",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    92
  title = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    93
  booktitle = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    94
  series = "LNCS 4108",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    95
  publisher = "Springer",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
    96
  year = 2006,
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    97
  available = { CB }
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    98
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
    99
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   100
% TPHOLs 1999
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   101
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   102
@inproceedings{KammullerEtAl1999,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   103
  author = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   104
  title = "Locales: A Sectioning Concept for {Isabelle}",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   105
  pages = "149--165",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   106
  crossref = "BertotEtAl1999",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   107
  available = { CB }
14586
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   108
}
7b8d56b4ac60 Added Locales Tutorial.
ballarin
parents:
diff changeset
   109
27063
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   110
@book{BertotEtAl1999,
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   111
  editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   112
  title = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   113
  booktitle = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   114
  publisher = "Springer",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   115
  series = "LNCS 1690",
d1d35284542f New version covering interpretation.
ballarin
parents: 16168
diff changeset
   116
  year = 1999
16168
adb83939177f Locales: new element constrains, parameter renaming with syntax,
ballarin
parents: 14586
diff changeset
   117
}