1.1 --- a/doc-src/manual.bib	Fri Sep 28 16:15:26 2001 +0200
     1.2 +++ b/doc-src/manual.bib	Fri Sep 28 16:42:26 2001 +0200
     1.3 @@ -137,6 +137,12 @@
     1.4    year =	 2000
     1.5  }
     1.6  
     1.7 +@INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
     1.8 +  crossref        = "tphols2000",
     1.9 +  title           = "Proof terms for simply typed higher order logic",
    1.10 +  author          = "Stefan Berghofer and Tobias Nipkow",
    1.11 +  pages           = "38--52"}
    1.12 +
    1.13  @InProceedings{Berghofer-Wenzel:1999:TPHOL,
    1.14    author = 	 {Stefan Berghofer and Markus Wenzel},
    1.15    title = 	 {Inductive datatypes in {HOL} --- lessons learned in
    1.16 @@ -1339,3 +1345,11 @@
    1.17    series	= {LNCS 1690},
    1.18    year		= 1999}
    1.19  
    1.20 +@PROCEEDINGS{tphols2000,
    1.21 +  editor          = "J. Harrison and M. Aagaard",
    1.22 +  booktitle       = "Theorem Proving in Higher Order Logics:
    1.23 +                     13th International Conference, TPHOLs 2000",
    1.24 +  series          = "Lecture Notes in Computer Science",
    1.25 +  volume          = 1869,
    1.26 +  year            = 2000,
    1.27 +  publisher       = "Springer-Verlag"}