Symbol lists are used in hiding reductions.
SYMB-ITEMS ::= symb-items SYMB-KIND SYMB+ SYMB-KIND ::= implicit | sorts | ops | preds SYMB ::= ID | QUAL-OP-NAME | QUAL-PRED-NAME
A list of symbols SYMB-ITEMS with implicit kinds SYMB-KIND is written simply:
SY1, ..., SYnOptionally, the list may be sectioned into sub-lists by inserting the keywords `sorts', `ops', `preds' (or their singular forms), which explicitly indicate that the subsequent symbols are of the corresponding kind:
sorts S1, ..., ops O1, ..., preds P1, ...As with signature declarations in basic specifications, there is no restriction on the order of the various sections of the list.
The list determines the set of listed symbols; the order in which symbols are listed is not significant (except regarding their position in relation to any specified kinds).