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.