\begin{thebibliography}{99}

\bibitem{SUPINFBledsoe} % OK
W.~W. Bledsoe.
\newblock A new method for proving certain {P}resburger formulas.
\newblock In {\em Advance Papers 4th Int. Joint Conf. on Artif. Intell.,
  Tbilisi, Georgia, U.S.S.R.}, pages 15--21, September 1975.

\bibitem{EfficFullyExpTP} % OK
R.~J. Boulton.
\newblock On efficiency in theorem provers which fully expand proofs into
  primitive inferences.
\newblock Technical Report 248, University of Cambridge Computer Laboratory,
  February 1992.

\bibitem{description} % OK
{\small DSTO} and {\small SRI} International,
{\em The HOL System: DESCRIPTION}, (1991).

\bibitem{reduce} % OK
J.~R.~Harrison.
\newblock The HOL reduce Library.
\newblock In {\em The HOL System: LIBRARIES}.
\newblock {\small DSTO} and {\small SRI} International, 1991.

\bibitem{VarElimHodes} % OK
L.~Hodes.
\newblock Solving problems by formula manipulation.
\newblock In {\em Advance Papers 2nd Int. Joint Conf. on Artif. Intell.,
  London}, pages 553--559. The British Computer Society, September 1971.
\newblock Revised version in Artificial Intelligence 3, North-Holland,
  Amsterdam, 1972, pages 165--174.

\bibitem{SUPINFShostak} % OK
R.~E. Shostak.
\newblock On the {SUP-INF} method for proving {P}resburger formulae.
\newblock {\em Journal of the ACM}, 24(4):529--543, October 1977.

\end{thebibliography}


