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

- prove
**A** - prove
**B**

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.

Thu Sep 14 08:45:18 EDT 1995