author | haftmann |
Fri, 14 Jun 2019 08:34:28 +0000 | |
changeset 70347 | e5cd5471c18a |
parent 67299 | ba52a058942f |
child 77812 | fb3d81bd9803 |
permissions | -rw-r--r-- |
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 | 15 |
@book{GKP_CM, |
16 |
author = {Graham, Ronald L. and Knuth, Donald E. and Patashnik, Oren}, |
|
17 |
title = {Concrete Mathematics: A Foundation for Computer Science}, |
|
18 |
year = {1994}, |
|
19 |
isbn = {0201558025}, |
|
20 |
edition = {2nd}, |
|
21 |
publisher = {Addison--Wesley}, |
|
22 |
address = {Boston, MA, USA}, |
|
23 |
} |
|
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 | 33 |
@book{card-book, |
34 |
title = {Introduction to {C}ardinal {A}rithmetic}, |
|
35 |
author = {M. Holz and K. Steffens and E. Weitz}, |
|
36 |
publisher = "Birkh{\"{a}}user", |
|
37 |
year = 1999, |
|
38 |
} |
|
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 | 47 |
} |
48 |
||
49 |
@InProceedings{paulin-tlca, |
|
50 |
author = {Christine Paulin-Mohring}, |
|
51 |
title = {Inductive Definitions in the System {Coq}: Rules and |
|
52 |
Properties}, |
|
53 |
crossref = {tlca93}, |
|
54 |
pages = {328-345}} |
|
55 |
||
56 |
@Proceedings{tlca93, |
|
57 |
title = {Typed Lambda Calculi and Applications}, |
|
58 |
booktitle = {Typed Lambda Calculi and Applications}, |
|
59 |
editor = {M. Bezem and J.F. Groote}, |
|
60 |
year = 1993, |
|
61 |
publisher = {Springer}, |
|
62 |
series = {LNCS 664}} |