For certain rules, we need to be able to control the free variables occuring
in the extract term.
The mechanism used to achieve this is that of * hidden* hypotheses.
A hypothesis is hidden when it is displayed enclosed in square brackets.
At the moment the only place where such hypotheses are added is in a subgoal
of the set elim rule.
The intended meaning of a hypothesis being hidden is that the name of the
hypothesis cannot appear free in the extracted term; that is, that it cannot
be used computationally.
Accordingly, a hidden hypothesis cannot be the object of an ` elim` or
` hyp` rule.
For the rules for which the extract term is the trivial term `
axiom`, the extract term contains no free variable references
and so all restrictions on the use of
hidden hypotheses can be removed.
The editor will remove the brackets from any hidden hypotheses
in displaying a goal of this form.

Thu Sep 14 08:45:18 EDT 1995