next up previous contents index
Next: ATOM Up: The Rules Previous: Hidden Assumptions

Shortcuts in the Presentation

With the exception of one of the direct computation rules, each of the rules has the property that the list of hypotheses in a subgoal is an extension of the hypothesis list of the goal. To highlight the new hypotheses and to save space, we will show only the new hypotheses in the subgoals. Also, we will not explicitly display trivial extraction terms, that is, extraction terms which are just axiom.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995