Next: Goal Labels
Up: Introduction
Previous: The Sequent
Nuprl proof terms (ML terms of type proof) can be
annotated with extra information which isn't relevant to the logical
correctness of a proof. Nuprl currently supports two kinds of annotations;
goal labels
and tactic arguments .
Karla Consroe
Wed Oct 23 13:48:45 EDT 1996