Symbol lists are used in hiding reductions.
[CHANGED:] []
SYMB-ITEMS ::= symb-items SYMB-KIND SYMB+
SYMB-KIND ::= implicit | sorts | ops | preds
SYMB ::= ID | QUAL-ID
QUAL-ID ::= qual-id ID TYPE
TYPE ::= OP-TYPE | PRED-TYPE | SORT
SY1, ..., SYn
[CHANGED:] Overloaded operation symbols and predicate symbols may be disambiguated by explicit qualification; when SYi is not qualified, the effect is as if all (sort, operation, or predicate) symbols declared with the same name in the current local environment are listed. A single sort occurring as a type in a qualified identifier QUAL-ID is interpreted as a constant operation type or unary predicate type, as determined by the local environment. [] Optionally, 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 f1, ..., 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 [CHANGED:] a set of qualified symbols, obtained from the listed symbols with reference to a given signature; [] the order in which symbols are listed is not significant (except regarding their position in relation to any specified kinds).