src/HOL/document/root.bib
author paulson <lp15@cam.ac.uk>
Fri, 22 Dec 2017 23:38:54 +0000
changeset 67270 f18c774acde4
parent 66893 ced164fe3bbd
child 67299 ba52a058942f
permissions -rw-r--r--
Merge
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66893
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     1
@book{Birkhoff79,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     2
  author =      {Garret Birkhoff},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     3
  title =       {Lattice Theory},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     4
  publisher =   {American Mathematical Society},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     5
  year=1979
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     6
}
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     7
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     8
@Book{davenport92,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
     9
  author =	 {H. Davenport},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    10
  title = 	 {The Higher Arithmetic},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    11
  publisher = 	 {Cambridge University Press},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    12
  year = 	 1992
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    13
}
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    14
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    15
@techreport{Gordon-TR68,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    16
  author = "Mike Gordon",
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    17
  title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    18
  institution = "University of Cambridge, Computer Laboratory",
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    19
  number = 68,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    20
  year = 1985
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    21
}
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    22
58623
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    23
@book{card-book,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    24
  title = {Introduction to {C}ardinal {A}rithmetic},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    25
  author = {M. Holz and K. Steffens and E. Weitz},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    26
  publisher = "Birkh{\"{a}}user",
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    27
  year = 1999,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    28
}
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    29
66893
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    30
@book{Nipkow-et-al:2002:tutorial,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    31
  author =      {T. Nipkow and L. C. Paulson and M. Wenzel},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    32
  title =       {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    33
  series =      {LNCS},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    34
  volume =      2283,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    35
  year =        2002,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    36
  publisher =   {Springer-Verlag}
58623
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    37
}
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    38
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    39
@InProceedings{paulin-tlca,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    40
  author	= {Christine Paulin-Mohring},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    41
  title		= {Inductive Definitions in the System {Coq}: Rules and
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    42
		 Properties},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    43
  crossref	= {tlca93},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    44
  pages		= {328-345}}
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    45
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    46
@Proceedings{tlca93,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    47
  title		= {Typed Lambda Calculi and Applications},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    48
  booktitle	= {Typed Lambda Calculi and Applications},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    49
  editor	= {M. Bezem and J.F. Groote},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    50
  year		= 1993,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    51
  publisher	= {Springer},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    52
  series	= {LNCS 664}}