The proof--editing facility supports top--down construction of proofs.
Goals are written as sequents ; they have the form
:
,
,
:
>> G, where the 
are the
hypotheses and
G is the conclusion.
To prove a goal ,
the user selects a rule for making progress toward achieving this goal,
and the system responds with a list of subgoals .
For example, if the goal is prove A&B and the rule selected
is ``and introduction,'' the system generates the following subgoals.
Proofs can be thought of as finite trees, where each node corresponds to the application of a logical rule. A proof can be read to the desired level of detail by descending into subtrees whose structure is interesting and passing over others.