doc-src/manual.bib

   title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
 		   Comparison}, 
   crossref	= {huet-plotkin91},
   pages		= {89-119}}
 
+
+@InProceedings{Berghofer-Wenzel:1999:TPHOL,
+  author = 	 {Stefan Berghofer and Markus Wenzel},
+  title = 	 {Inductive datatypes in HOL --- lessons learned in Formal-Logic Engineering},
+  booktitle = 	 {Theorem Proving in Higher Order Logics (TPHOLs'99)},
+  series =	 LNCS,
+  year =	 1999,
+  publisher =	 Springer,
+  note =	 {to appear}
+}
+
 @book{Bird-Wadler,author="Richard Bird and Philip Wadler",
 title="Introduction to Functional Programming",publisher=PH,year=1988}
 
 @Article{boyer86,
   author	= {Robert Boyer and Ewing Lusk and William McCune and Ross

   year		= 1994,
   month		= aug}
 
 %W
 
+
+@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
+}
+
 @book{principia,
   author	= {A. N. Whitehead and B. Russell},
   title		= {Principia Mathematica},
   year		= 1962,
   publisher	= CUP,