Major Section: EVENTS
Examples: (deflabel interp-section :doc ":Doc-Section ...") General Form: (deflabel name :doc doc-string)where
nameis a new symbolic name (see name) and
doc-stringis an optional documentation string (see doc-string). This event adds the documentation string for symbol
docdatabase. By virtue of the fact that
deflabelis 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.
Deflabelevents 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.