# HG changeset patch # User wenzelm # Date 1013542343 -3600 # Node ID 2896f88180b9ba5581791b99af9f165a346adb5e # Parent b9635eb8a4489d1bb7b8866f46d819f667524095 added isabelle-hol-book; added tphols2001; tuned tphols2000; diff -r b9635eb8a448 -r 2896f88180b9 doc-src/manual.bib --- 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}