The first part of this paper is a guided tour through the real library with
emphasis on the definitions, a handful of useful theorems, and the proof of the
intermediate value theorem. Afterwards is a section giving detailed
descriptions of the special-purpose tactics that were written in conjunction
with the rationals and the reals. Users interested in developing theories in
analysis should find both sections helpful.