(primitive) remove one or more abbreviations
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
Remark: The instruction fails if at least one of the arguments fails to be a variable that abbreviates a term.
Also see ACL2-pc::add-abbreviation for a discussion of abbreviations in general, and see ACL2-pc::show-abbreviations.