1\begin{thebibliography}{99}
2
3\bibitem{SUPINFBledsoe} % OK
4W.~W. Bledsoe.
5\newblock A new method for proving certain {P}resburger formulas.
6\newblock In {\em Advance Papers 4th Int. Joint Conf. on Artif. Intell.,
7  Tbilisi, Georgia, U.S.S.R.}, pages 15--21, September 1975.
8
9\bibitem{EfficFullyExpTP} % OK
10R.~J. Boulton.
11\newblock On efficiency in theorem provers which fully expand proofs into
12  primitive inferences.
13\newblock Technical Report 248, University of Cambridge Computer Laboratory,
14  February 1992.
15
16\bibitem{description} % OK
17{\small DSTO} and {\small SRI} International,
18{\em The HOL System: DESCRIPTION}, (1991).
19
20\bibitem{reduce} % OK
21J.~R.~Harrison.
22\newblock The HOL reduce Library.
23\newblock In {\em The HOL System: LIBRARIES}.
24\newblock {\small DSTO} and {\small SRI} International, 1991.
25
26\bibitem{VarElimHodes} % OK
27L.~Hodes.
28\newblock Solving problems by formula manipulation.
29\newblock In {\em Advance Papers 2nd Int. Joint Conf. on Artif. Intell.,
30  London}, pages 553--559. The British Computer Society, September 1971.
31\newblock Revised version in Artificial Intelligence 3, North-Holland,
32  Amsterdam, 1972, pages 165--174.
33
34\bibitem{SUPINFShostak} % OK
35R.~E. Shostak.
36\newblock On the {SUP-INF} method for proving {P}resburger formulae.
37\newblock {\em Journal of the ACM}, 24(4):529--543, October 1977.
38
39\end{thebibliography}
40
41
42