--- a/doc-src/manual.bib Tue Feb 12 20:31:40 2002 +0100
+++ b/doc-src/manual.bib Tue Feb 12 20:32:23 2002 +0100
@@ -147,6 +147,11 @@
year = 2000
}
+@InProceedings{Bauer-Wenzel:2001,
+ author = {Gertrud Bauer and Markus Wenzel},
+ title = {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
+ crossref = {tphols2001}}
+
@INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
crossref = "tphols2000",
title = "Proof terms for simply typed higher order logic",
@@ -864,6 +869,13 @@
year = 1994,
note = {LNCS 828}}
+@Book{isabelle-hol-book,
+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+ title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
+ publisher = {Springer},
+ year = 2002,
+ note = {LNCS 2283}}
+
@InCollection{paulson-markt,
author = {Lawrence C. Paulson},
title = {Tool Support for Logics of Programs},
@@ -1380,11 +1392,16 @@
series = {LNCS 1690},
year = 1999}
-@PROCEEDINGS{tphols2000,
- editor = "J. Harrison and M. Aagaard",
- booktitle = "Theorem Proving in Higher Order Logics:
- 13th International Conference, TPHOLs 2000",
- series = "Lecture Notes in Computer Science",
- volume = 1869,
- year = 2000,
- publisher = "Springer-Verlag"}
+@Proceedings{tphols2000,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},
+ editor = {J. Harrison and M. Aagaard},
+ series = {LNCS 1869},
+ year = 2000}
+
+@Proceedings{tphols2001,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
+ editor = {R. J. Boulton and P. B. Jackson},
+ series = {LNCS 2152},
+ year = 2001}