diff -r 7067101463c0 -r 0b231e0fd7d7 doc-src/manual.bib
--- a/doc-src/manual.bib	Fri Sep 28 16:15:26 2001 +0200
+++ b/doc-src/manual.bib	Fri Sep 28 16:42:26 2001 +0200
@@ -137,6 +137,12 @@
   year =	 2000
 }
 
+@INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
+  crossref        = "tphols2000",
+  title           = "Proof terms for simply typed higher order logic",
+  author          = "Stefan Berghofer and Tobias Nipkow",
+  pages           = "38--52"}
+
 @InProceedings{Berghofer-Wenzel:1999:TPHOL,
   author = 	 {Stefan Berghofer and Markus Wenzel},
   title = 	 {Inductive datatypes in {HOL} --- lessons learned in
@@ -1339,3 +1345,11 @@
   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"}