\begin{thebibliography}{9}

\bibitem{melham} % OK
T.\ F.\ Melham,
{\it The HOL sets library},
University of Cambridge Computer Laboratory,
October 1991.

\bibitem{description} % OK
University of Cambridge Computer Laboratory,
{\it The HOL System: DESCRIPTION}, revised edition, 1991.

\end{thebibliography}


