Gets the closing bracket given the opning one

This is the term fixity resetting command for variable/constant names. It takes a string, and removes the registered term fixity of the string name, so that any variables or constants with that name get written with nonfix fixity. A note of the fixity change is reported, and unit is returned.

This is the type fixity resetting command for type constant names. It takes a string, and removes the registered type fixity of the string name, so that any type constants with that name get written with nonfix fixity. A note of the fixity change is reported, and unit is returned.

This is the enumeration bracket setting command. It takes two pairs of strings, where the first pair is the name of an enumeration insertion operator constant and the name of an enumeration empty structure constant, and the second pair is the name of the opening and closing enumeration brackets to be associated with these constants. The brackets are registered as the enumeration brackets corresponding to the supplied constants, and become reserved words of the HOL language. A note of the bracket declaration is reported, and unit is returned.

This is the term fixity setting command for variable/constant names. It takes a string and a fixity, and registers the term fixity of the string name as the supplied fixity, so that any variables or constants with that name get written with that fixity. Supplying a name that is currently registered with a fixity that is not nonfix will cause failure (except in benign resetting to the same fixity). A note of the fixity change is reported, and unit is returned.

This is the type fixity setting command for type constant names. It takes a string and a fixity, and registers the type fixity of the string name as the supplied fixity, so that any type constants with that name get written with that fixity. Supplying a name that is currently registered with a fixity that is not nonfix will cause failure (except in benign resetting to the same fixity). A note of the fixity change is reported, and unit is returned.

The enumeration bracket database is a secondary database, used during parsing for looking up the empty structure constant name for a given enumeration bracket. This is implemented as a dynamic lookup tree, indexed by enumeration bracket. There are entries for each opening bracket, each closing bracket and for each pair of concatenated corresponding opening and closing brackets. These concatenated pair entries are used by the term quotation parser, to allow empty enumerations appearing in term quotations to have no space between the opening and closing enumeration brackets.

The main enumeration database registers the associations between insertion operator and empty structure constants and opening and closing enumeration brackets. It is implemented as a dynamic lookup tree, indexed by empty structure constant name.

The term fixity database registers the fixity of var/const identifiers. It is implemented as a dynamic lookup tree, indexed by identifier name. Identifiers not occurring in the database have default nonfix fixity.

The type fixity database registers the fixity of type constant identifiers. It is implemented as a dynamic lookup tree, indexed by type constant name. Identifiers not occurring in the database have default nonfix fixity.