This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.2.
The sorts appearing in a subsort declaration should be using instead of declaring occurrences. The same holds for subsorts appearing as alternatives in datatype declarations.
The rest of this document has not yet been converted to Hypertext; please refer to the FTP directory indicated above for the full document.