5 Display Format

Symbols

used in the input of types and formulae are displayed as follows:

Input:	*	->	forall	exists	/\	\/	=>	<=>	not	in	.
Display:	×	->	forall	exists	/\	\/	=>	<=>	¬	in	·

When a mathematical symbol is not available (e.g., when browsing HTML on WWW) the input syntax for it may be displayed instead. Moreover, characters whose display format is in ISO Latin-1 may always be used for input. This allows the direct input of the symbols displayed as `¬', `×', and ` · ', and ensures that the text of a specification as shown by a WWW browser is valid input syntax (at least in the absence of display annotations).

Keywords

are generally displayed in a boldface font: sorts, ops, etc. Within a FORMULA, however, they are displayed in the same font as identifiers: if, true, false, def, as, op, pred.

Identifiers

are displayed with letters in italic: f, x, Very_Long_Identifier. Non-letter characters in identifiers are displayed as faithfully as possible--note that whereas all printable ISO Latin-1 characters are allowed for input, some of them are missing in the standard fonts used by formatters. The components of compound identifiers are displayed with the enclosing brackets (not as subscripts): List[Item], Pair[Item,List[Item]].

Comments

(see Section 6.1) are generally displayed in the same font as ordinary informal text that might appear before and after CASL specification (but note that this may be overruled by formatting instructions occurring in the comment text). The display of a comment need not preserve the original line-breaks of the input; but each line of the displayed comment must always start with `%%'.

Annotations

(see Section 6.2) need not be displayed at all.