remove one or more abbreviations
Major Section: PROOF-CHECKER-COMMANDS
Examples:
remove-abbreviations -- remove all abbreviations
(remove-abbreviations v w)
-- assuming that V and W currently abbreviate
terms, then they are ``removed'' in the
sense that they are no longer considered to
abbreviate those terms
General Forms:
(remove-abbreviations &rest vars)
If vars is not empty (i.e., not nil), remove the variables in vars
from the current list of abbreviations, in the sense that each
variable in vars will no longer abbreviate a term.Remark: The instruction fails if at least one of the arguments fails to be a variable that abbreviates a term.
See also the documentation for add-abbreviation, which contains a
discussion of abbreviations in general, and show-abbreviations.
