LOCAL-SPEC ::= local-spec SPEC SPEC
A local specification LOCAL-SPEC is written:
local SP1 within SP2
It is equivalent to writing:
{ SP1 then SP2 } hide SY1, ..., SYnwhere SY1, ..., SYn are all the symbols declared by SP1 that are not already in the current local environment. Thus the symbols SY1, ..., SYn are only for local use in (SP1 and) SP2. The hiding must not affect symbols that are declared only in SP2 (thus operation or predicate symbols declared in SP2 should not have sorts declared by SP1 in their profiles).