A tactic is a strategy for proving the current goal given the current hypotheses. The user specifies a tactic to apply and the tactic runs on the current goal and hypotheses to create a set of new subgoals. The user then specifies tactics to use to prove the new subgoals. This process is repeated until every subgoal is proved, in which case the entire theorem is proved. Nuprl also has objects called conversions which can be used to rewrite clauses or parts of clauses.
Conversions are rewrite rules that take a term and rewrite it to an equivalent term.
These may be used to manipulate hypotheses to facilitate matching. Once a conversion has been defined, tactics are used to run these conversions and perform the actual rewriting. The only subgoals which are shown are those that remain to be proved after all of the listed tactics are run one the specified subgoals. Nuprl allows the user to make reference to previously proved theorems, or, as Nuprl refers to them, lemmas. A lemma is invoked by using the name under which the theorem was proved as an argument to a tactic that acts on lemmas.