diff -r 613724c2ee6b -r 48a66203192c doc-src/manual.bib
--- 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},