src/HOL/document/root.bib
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 77812 fb3d81bd9803
permissions -rw-r--r--
tuned;
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
67299
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    15
@book{GKP_CM,
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    16
 author = {Graham, Ronald L. and Knuth, Donald E. and Patashnik, Oren},
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    17
 title = {Concrete Mathematics: A Foundation for Computer Science},
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    18
 year = {1994},
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    19
 isbn = {0201558025},
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    20
 edition = {2nd},
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    21
 publisher = {Addison--Wesley},
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    22
 address = {Boston, MA, USA},
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    23
}
ba52a058942f prefer formal citations;
wenzelm
parents: 66893
diff changeset
    24
66893
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    25
@techreport{Gordon-TR68,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    26
  author = "Mike Gordon",
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    27
  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
    28
  institution = "University of Cambridge, Computer Laboratory",
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    29
  number = 68,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    30
  year = 1985
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    31
}
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    32
58623
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    33
@book{card-book,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    34
  title = {Introduction to {C}ardinal {A}rithmetic},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    35
  author = {M. Holz and K. Steffens and E. Weitz},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    36
  publisher = "Birkh{\"{a}}user",
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    37
  year = 1999,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    38
}
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    39
66893
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    40
@book{Nipkow-et-al:2002:tutorial,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    41
  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
    42
  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
    43
  series =      {LNCS},
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    44
  volume =      2283,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    45
  year =        2002,
ced164fe3bbd derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents: 58623
diff changeset
    46
  publisher =   {Springer-Verlag}
58623
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    47
}
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    48
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    49
@InProceedings{paulin-tlca,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    50
  author	= {Christine Paulin-Mohring},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    51
  title		= {Inductive Definitions in the System {Coq}: Rules and
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    52
		 Properties},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    53
  crossref	= {tlca93},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    54
  pages		= {328-345}}
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    55
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    56
@Proceedings{tlca93,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    57
  title		= {Typed Lambda Calculi and Applications},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    58
  booktitle	= {Typed Lambda Calculi and Applications},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    59
  editor	= {M. Bezem and J.F. Groote},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    60
  year		= 1993,
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    61
  publisher	= {Springer},
2db1df2c8467 more bibtex entries;
wenzelm
parents: 27367
diff changeset
    62
  series	= {LNCS 664}}
77812
fb3d81bd9803 some remarks on division
haftmann
parents: 67299
diff changeset
    63
fb3d81bd9803 some remarks on division
haftmann
parents: 67299
diff changeset
    64
@article{leijen01,
fb3d81bd9803 some remarks on division
haftmann
parents: 67299
diff changeset
    65
  author  = {Leijen, Daan},
fb3d81bd9803 some remarks on division
haftmann
parents: 67299
diff changeset
    66
  title   = {Division and Modulus for Computer Scientists},
fb3d81bd9803 some remarks on division
haftmann
parents: 67299
diff changeset
    67
  year    = 2001,
fb3d81bd9803 some remarks on division
haftmann
parents: 67299
diff changeset
    68
  url     = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf}}