Deflabel
Build a landmark
Examples:
(deflabel interp-section)
General Form:
(deflabel name)
where name is a new symbolic name (see name). By virtue of the
fact that deflabel is an event, it marks the current history with
the name. 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.
