The HOL reals Library

John Harrison.

Unpublished manual, 21st July 1992.


This is the online manual for the HOL reals library, included in the standard release of the Cambridge HOL system. It isn't a particularly good read, and more information about the development can be found in the author's paper.

DVI or PostScript