Library Window

The library window displays a linear segment of the library, one object per line. When theories are loaded into the library, they are always placed in a linear order.

  
Figure: The Library Display Window

An example library display is shown in Figure . From left to right each line contains:

status 

One character: ?  for raw, -  for bad, #  for incomplete and *  for complete.

kind 

One character: R  for rule , t and T  for theorem , A  for abstraction , M  for ML , D  for display , L  for lattice (the old name we used for the precedence object) and C  for comment . The lower case `` t '' is used for compressed theorems and the upper case `` T ''for expanded theorems.

name 

The name of the object.

summary 

The first few characters of the object's contents.