		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::show-abbreviations

(macro) display the current abbreviations

Examples:
(show-abbreviations v w)
   -- assuming that v and w currently abbreviate terms,
      then this instruction displays them together with
      the terms they abbreviate
show-abbreviations
   -- display all abbreviations

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

General Form:
(show-abbreviations &rest vars)

Display each argument in vars together with the term it abbreviates (if any). If there are no arguments, i.e. the instruction is simply show-abbreviations, then display all abbreviations together with the terms they abbreviate.

If the term abbreviated by a variable, say v, contains a proper subterm that is also abbreviate by (another) variable, then both the unabbreviated term and the abbreviated term (but not using (? v) to abbreviate the term) are displayed with together with v.