proofs are sequent proofs organized
in a refinement style.
In other words they are trees where each node contains a * goal*
and a * rule application*.
The children of a node are the * subgoals*
of their parent; in order to prove the parent it is sufficient to prove
the children.
(
automatically generates the children, given their parent and the rule
to be applied; it is never necessary to type them in.)
Not all goals have subgoals; for example, a goal proved by ` hyp`
does not.
Also, an * incomplete* goal (one whose rule is bad or missing) has no
subgoals.

In what follows the * main goal* (* the* goal for short)
is the goal of the current node;
* a* goal is either the main goal or one of its subgoals.

- Basics of the Proof Editor
- Motion within a Proof Node
- Motion within the Proof Tree
- Initiating a Refinement
- Showing Goals, Subgoals and Rules
- Invoking Transformation Tactics

Thu Sep 14 08:45:18 EDT 1995