Library Display

  The library is a list of the objects defined by the user and may contain the theorems, definitions, evaluation bindings and ML code. Information about the library objects is displayed in the library  window. The jump and scroll commands change what is being displayed in the library window, while the move command changes the order of library objects. The move command is often used to make sure that objects occur before their uses; this is important for correct library reloading.

jump object

  The library is redisplayed so that the specified entry is visible.

move objects place

  The specified library objects are moved to the position just after the specified place.

scroll

  The library window is moved the specified number of entries, in the specified direction. The default direction is down, and the default number of entries is one. For example, scroll 5 shifts the window down five entries, while scroll up shifts the window up one entry.