next up previous contents index
Next: The Command Language Up: No Title Previous: The Auto--tactic

System Description

This  chapter describes various parts of the system: the command language, library, windows, editors and notation definitions. With the command language one can create, delete and manipulate library objects, evaluate terms, call up the editors, and ``check'' (i.e., parse and generate code for) objects. The library contains the various user--defined objects, the editors provide ways to modify them, definitions make them more readable, and the window system makes the editors more useful.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995