In Nuprl
all theorems consist of goal statements, where a goal statement is
similar to sequents used in natural deduction style inference systems. The
form of a goal statement is H >> T, where H is a hypothesis list and T
is a formula in the Nuprl
logic. The symbols >> separate the
hypotheses from the conclusion
and thus correspond to the 
symbol
used in logic. Top--level goals must have empty hypothesis lists; this
prevents the user from introducing inconsistent hypotheses.
Theorems also cannot contain free variables; in the terminology of
chapter 2, this means that all top--level goals must contain closed terms to the right of the
>> symbol.