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

(deflabel interp-section
   ":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 database. 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.