DEFLABEL

build a landmark and/or add a documentation topic 
Major Section:  EVENTS


Examples:
(deflabel interp-section
   :doc
   ":Doc-Section ...")


General Form:
(deflabel name :doc doc-string)
where name is a new symbolic name (see name) and doc-string is an optional documentation string (see doc-string). This event adds the documentation string for symbol name to the :doc data base. By virtue of the fact that deflabel is an event, it also marks the current history with the name. Thus, even undocumented labels are convenient as landmarks in a proof development. For example, you may wish to undo back through some label or compute a theory expression (see theories) in terms of some labels. Deflabel events are never considered redundant. See redundant-events.

See defdoc for a means of attaching a documentation string to a name without marking the current history with that name.