--- a/doc-src/manual.bib Mon Jul 19 16:47:24 1999 +0200
+++ b/doc-src/manual.bib Mon Jul 19 16:53:02 1999 +0200
@@ -91,12 +91,9 @@
@InProceedings{Berghofer-Wenzel:1999:TPHOL,
author = {Stefan Berghofer and Markus Wenzel},
- title = {Inductive datatypes in {HOL} --- lessons learned in {F}ormal-{L}ogic {E}ngineering},
- booktitle = {Theorem Proving in Higher Order Logics (TPHOLs'99)},
- series = LNCS,
- year = 1999,
- publisher = Springer
-}
+ title = {Inductive datatypes in {HOL} --- lessons learned in
+ {F}ormal-{L}ogic {E}ngineering},
+ crossref = {tphols99}}
@book{Bird-Wadler,author="Richard Bird and Philip Wadler",
title="Introduction to Functional Programming",publisher=PH,year=1988}
@@ -367,6 +364,12 @@
pages = {205-216},
publisher = {Elsevier}}
+@InProceedings{Harrison:1996:MizarHOL,
+ author = {J. Harrison},
+ title = {A {Mizar} Mode for {HOL}},
+ pages = {203--220},
+ crossref = {tphols96}}
+
%K
@InProceedings{kammueller-locales,
@@ -469,12 +472,9 @@
@InProceedings{NaraschewskiW-TPHOLs98,
author = {Wolfgang Naraschewski and Markus Wenzel},
title =
-{Object-Oriented Verification based on Record Subtyping in Higher-Order Logic},
- booktitle = {Theorem Proving in Higher Order Logics (TPHOLs'98)},
- publisher = Springer,
- volume = 1479,
- series = LNCS,
- year = 1998}
+{Object-Oriented Verification based on Record Subtyping in
+ Higher-Order Logic},
+ crossref = {tphols98}}
@inproceedings{nazareth-nipkow,
author = {Dieter Nazareth and Tobias Nipkow},
@@ -800,6 +800,15 @@
publisher = {Addison-Wesley},
year = 1990}
+@InProceedings{Rudnicki:1992:MizarOverview,
+ author = {P. Rudnicki},
+ title = {An Overview of the {MIZAR} Project},
+ booktitle = {1992 Workshop on Types for Proofs and Programs},
+ year = 1992,
+ organization = {Chalmers University of Technology},
+ publisher = {Bastad}
+}
+
%S
@inproceedings{saaltink-fme,
@@ -833,6 +842,27 @@
crossref = {huet-plotkin93},
pages = {317-338}}
+@TechReport{Syme:1997:DECLARE,
+ author = {D. Syme},
+ title = {{DECLARE}: A Prototype Declarative Proof System for Higher Order Logic},
+ institution = {University of Cambridge Computer Laboratory},
+ year = 1997,
+ number = 416
+}
+
+@PhdThesis{Syme:1998:thesis,
+ author = {D. Syme},
+ title = {Declarative Theorem Proving for Operational Semantics},
+ school = {University of Cambridge},
+ year = 1998,
+ note = {Submitted}
+}
+
+@InProceedings{Syme:1999:TPHOL,
+ author = {D. Syme},
+ title = {Three Tactic Theorem Proving},
+ crossref = {tphols99}}
+
%T
@book{takeuti87,
@@ -848,6 +878,13 @@
publisher = {Addison-Wesley},
year = 1991}
+@Unpublished{Trybulec:1993:MizarFeatures,
+ author = {A. Trybulec},
+ title = {Some Features of the {Mizar} Language},
+ note = {Presented at a workshop in Turin, Italy},
+ year = 1993
+}
+
%V
@Unpublished{voelker94,
@@ -859,16 +896,17 @@
%W
+@InProceedings{Wenzel:1999:TPHOL,
+ author = {Markus Wenzel},
+ title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
+ crossref = {tphols99}}
@InProceedings{Wenzel:1997:TPHOL,
author = {Markus Wenzel},
title = {Type Classes and Overloading in Higher-Order Logic},
- booktitle = {Theorem Proving in Higher Order Logics (TPHOLs'97)},
- year = 1997,
- series = LNCS,
- volume = 1275,
- publisher = Springer
-}
+ crossref = {tphols97}}
+
+
@book{principia,
author = {A. N. Whitehead and B. Russell},
@@ -1045,6 +1083,20 @@
series = {LNCS 1125},
year = 1996}
+@Proceedings{tphols97,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
+ editor = {Elsa L. Gunter and Amy Felty},
+ series = {LNCS 1275},
+ year = 1997}
+
+@Proceedings{tphols98,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
+ editor = {Jim Grundy and Malcom Newey},
+ series = {LNCS 1479},
+ year = 1998}
+
@Proceedings{tphols99,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},