| 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-- |
|
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 | 23 |
@book{card-book,
|
24 |
title = {Introduction to {C}ardinal {A}rithmetic},
|
|
25 |
author = {M. Holz and K. Steffens and E. Weitz},
|
|
26 |
publisher = "Birkh{\"{a}}user",
|
|
27 |
year = 1999, |
|
28 |
} |
|
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 | 37 |
} |
38 |
||
39 |
@InProceedings{paulin-tlca,
|
|
40 |
author = {Christine Paulin-Mohring},
|
|
41 |
title = {Inductive Definitions in the System {Coq}: Rules and
|
|
42 |
Properties}, |
|
43 |
crossref = {tlca93},
|
|
44 |
pages = {328-345}}
|
|
45 |
||
46 |
@Proceedings{tlca93,
|
|
47 |
title = {Typed Lambda Calculi and Applications},
|
|
48 |
booktitle = {Typed Lambda Calculi and Applications},
|
|
49 |
editor = {M. Bezem and J.F. Groote},
|
|
50 |
year = 1993, |
|
51 |
publisher = {Springer},
|
|
52 |
series = {LNCS 664}}
|