		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::remove-abbreviations

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

Also see ACL2-pc::add-abbreviation for a discussion of abbreviations in general, and see ACL2-pc::show-abbreviations.