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 termsIf vars is not empty (i.e., not
General Forms: (remove-abbreviations &rest vars)
nil), remove the variables in
varsfrom the current list of abbreviations, in the sense that each variable in
varswill no longer abbreviate a term.
Note: 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