A display annotation is of the form `%!...%!'. It associates a particular input symbol (an ID) with formatting instructions for its display, using the same notation for delimiting formatting languages as used for comments.
When the display annotation immediately follows a declared ID in a sort, operation, or variable declaration, the input symbol concerned is taken to be that ID, and the body of the display annotation gives the formatting instructions. E.g.,
determines how the ID input as `div' is to be displayed by LaTeX and HTML formatters (÷), with other formatters by default displaying the input symbol as written.... div %!<latex>$\div$<html>÷%!
Further details concerning the use of formatting instructions in annotations are given in [BCKB+98].