John Harrison.
Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order
Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium. Volume A-20
of IFIP Transactions A: Computer Science and Technology, North-Holland, pp.
145-164, 1992.

**NB! This paper is superseded by a
newer version
**

## Abstract:

We describe a construction of the real numbers in the HOL theorem-prover by
strictly definitional means using a version of Dedekind's method. We also
outline the theory of mathematical analysis that has been built on top of it,
and discuss current and potential applications in verification and computer
algebra.
## Bibtex entry:

@INPROCEEDINGS{harrison-hol92,
crossref = "hol92",
author = "John Harrison",
title = "Constructing the Real Numbers in {HOL}",
pages = "145--164"}
@PROCEEDINGS{hol92,
editor = "Luc J. M. Claesen and Michael J. C. Gordon",
booktitle = "Proceedings of the {IFIP} {TC10/WG10.2}
International Workshop on Higher Order Logic Theorem
Proving and its Applications",
series = "IFIP Transactions A: Computer Science and
Technology",
volume = "A-20",
address = "IMEC, Leuven, Belgium",
date = "September 1992",
year = 1992,
publisher = "North-Holland"}