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 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.
