doc-src/manual.bib

   title		= {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
 		   Comparison}, 
   crossref	= {huet-plotkin91},
   pages		= {89-119}}
 
+@InProceedings{Bauer-Wenzel:2000:HB,
+  author = 	 {Gertrud Bauer and Markus Wenzel},
+  title = 	 {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
+      {I}sabelle/{I}sar},
+  booktitle = 	 {Types for Proofs and Programs: TYPES'99},
+  series =	 {LNCS},
+  year =	 2000,
+  note =	 {To appear}
+}
 
 @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},

 
 @manual{isabelle-axclass,
   author	= {Markus Wenzel},
   title		= {Using Axiomatic Type Classes in {I}sabelle},
   institution	= {TU Munich},
+  year          = 2000,
   note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
 
 
 @InProceedings{Wenzel:1999:TPHOL,
   author = 	 {Markus Wenzel},