Introduction

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.