A list SORT-ITEMS of sort declarations determines one or more sorts. A list OP-ITEMS of operation declarations and/or definitions determines one or more operation symbols, and possibly some sentences; similarly for a list PRED-ITEMS of predicate declarations and/or definitions. Operation and predicate symbols may be overloaded, being declared with several different profiles in the same local environment. A list DATATYPE-ITEMS of datatype declarations determines one or more sorts together with some constructor and (optional) selector operations, and sentences defining the selector operations on the values given by the constructors with which they are associated.