A Nuprl tactic generates various kinds of subgoals, and often subsequent tactics want to discriminate on subgoal kind. Sometimes a subgoal's kind can be deduced directly from its structure, but this can be a error-prone process and so tactics attach explicit labels to subgoals indicating their kind. Labels take the form of an ML token, and an optional number. Examples of labels are main, upcase and wf. Most descriptions of tactics include information on subgoal labelling. It is also a simple matter to find out what labels are generated by experimentation.
The tacticals which discriminate on labels are described in the
tacticals section below. For convenience, labels are divided into the
the classes main and aux . The discriminating
tacticals allow one to select either subgoals with a particular label,
or subgoals of one of the two classes. One selects a class by
using one of the class names main or aux.
Sometimes tactics generate a set of subgoals which are all the same kind, but where the order of the subgoals is important. The number labels are used to discriminate between these subgoals.
Labels used not to be visible when editing proofs with the proof editor and are therefore sometimes known as hidden labels .
AddHiddenLabel lab
AddHiddenLabelAndNumber lab i
UnhideLabel
See Section 
for how to discriminate on labels.