\begin{thebibliography}{10}
\bibitem{bm88book}
Robert~S. Boyer and J~Strother Moore.
\newblock {\em A Computational Logic Handbook}.
\newblock Academic Press, 1988.
\bibitem{charniak80}
E.~Charniak, C.~K. Riesbeck, and D.~V. McDermott.
\newblock {\em Artificial Intelligence Programming}.
\newblock Lawrence Erlbaum Associates, 1980.
\bibitem{debruijn72}
N.~G. de~Bruijn.
\newblock Lambda calculus notation with nameless dummies, a tool for automatic
formula manipulation, with application to the {Church-Rosser Theorem}.
\newblock {\em Indagationes Mathematicae}, 34:381--392, 1972.
\bibitem{OBJ}
K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer.
\newblock Principles of {OBJ2}.
\newblock In {\em Symposium on Principles of Programming Languages}, pages
52--66, 1985.
\bibitem{martin-nipkow}
Ursula Martin and Tobias Nipkow.
\newblock Ordered rewriting and confluence.
\newblock In Mark~E. Stickel, editor, {\em 10th International Conference on
Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990.
\bibitem{nipkow-patterns}
Tobias Nipkow.
\newblock Functional unification of higher-order patterns.
\newblock In M.~Vardi, editor, {\em Eighth Annual Symposium on Logic in
Computer Science}, pages 64--74. {\sc ieee} Computer Society Press, 1993.
\bibitem{nipkow-prehofer}
Tobias Nipkow and Christian Prehofer.
\newblock Type reconstruction for type classes.
\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.
\bibitem{nordstrom90}
Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
\newblock Oxford University Press, 1990.
\bibitem{paulson91}
Lawrence~C. Paulson.
\newblock {\em {ML} for the Working Programmer}.
\newblock Cambridge University Press, 1991.
\bibitem{paulson-ml2}
Lawrence~C. Paulson.
\newblock {\em {ML} for the Working Programmer}.
\newblock Cambridge University Press, 2nd edition, 1996.
\bibitem{pelletier86}
F.~J. Pelletier.
\newblock Seventy-five problems for testing automatic theorem provers.
\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
\end{thebibliography}