Use the NEW button in MainMenu to open an object creation utility. (Try it now.)

This gives you some choices. As usual, if you don't select an option from first-option |second-option |more-options, then the first option is used.

The "newob" option creates and views a new object of the specified kind at the indicated place.
The "newsegment" option creates some objects for managing a contiguous section of new objects.

A place is indicated as follows:

LAST means put it AFTER ALL other objects.

(After: [ob name]) means put it AFTER the named object.

(Before: [ob name]) means put it BEFORE the named object.

DEFAULT means to use a default previously specified by the user.

When "newsegment" is used, the DEFAULT is for new objects to be inserted at the end of the new library segment. The DEFAULT can also be set via a button in the object creation menu that NEW raised.

DEFINING new operators along with their display forms and well-formedness theorems:

Operator definitions or declarations are made in ABS objects. So create an ABSobject with whatever name you like, normally mnemonic for the operator, edit the definition and verify the object with `(c-v)'.
This will raise a utility prompting you for creation of display forms and usually well-formedness lemmas specifying the operator type.

See the following for how to create and edit definitions, display form specifications, and well-formedness lemmas.

Edit Operator Definitions (ABS)
Edit Display Form Specs
Edit Proofs