Every object has associated with it a status , either raw , bad , incomplete or complete , indicating the current state of the object. A raw status means an object has been changed but not yet checked. A bad status means an object has been checked and found to contain errors. An incomplete status is meaningful only for proofs and signifies that the proof contains no errors but has not been finished. A complete status indicates that the object is correct and complete.
An entry for an object in the library contains its status, type, name and a summary of the contents. The status is encoded as a single character: ? for raw, - for bad, # for incomplete and * for complete. A typical entry might be the following.
,--------------------------------------------------------,
| Library |
|--------------------------------------------------------|
| * simple |
| THM >> int in U1 |
| |
| |
'--------------------------------------------------------'
The library window provides the mechanism for viewing these entries.
The entries are kept in a linear order,
and at any one time
a section of the entries is visible in the library window.
The library placement commands described in section 7.1 can be used to
change the order of the entries
and to move the window around within the list of entries.