ACL2-PC::REMOVE-ABBREVIATIONS

(primitive) 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.

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