The library is a list of all the objects defined by the user and includes theorems, definitions, evaluation bindings and ML code. The library window displays information about the various objects--- their names, types, statuses and summary descriptions. In this section we give a short description of the different kinds of objects and their statuses.