A label annotation is of the form `%[ID,...,ID]'. [CHANGED:] It may be written in various lists of items (e.g., declarations or axioms), [] immediately preceding the item to which it is to be attached.
