Appendix C: Changes from the Tentative Design

Only the major changes are listed.

• Carrier sets are now always non-empty.
• The notion of explicitly-sorted term has been eliminated.
• Redeclaration of the same symbol is now allowed, both in lists of basic items and in extensions.
• The same identifier may be used simultaneously to name several different kinds of entities, e.g., a sort and a function.
• Visibility is now non-linear in lists of basic items.
• The construct for sort generation has been changed so that it applies to a list SIG-DECL+.
• Attributions are now included as components of function declarations.
• A construct for defining functions (including constants) has been included.
• Type definition groups have been eliminated from structured specifications, and type definitions (now called datatype declarations) as basic items no longer involve free extensions. Multiple selectors of the same sort now have to be specified separately.
• Subsort declarations now declare sorts as well as their embedding, and the syntax has been simplified.
• Local specifications have been introduced, both as basic and structured specifications.
• The syntax of EXTENSION has been simplified, and analogously in generic specifications.
• Different syntactic categories for specification names have been introduced.
• Architectural specifications can now be used in ordinary specifications.
• Unit definitions have been introduced.