The theorem OUTPUT causes the current subterm to be displayed. It is always regarded as succeeding. A keystroke is necessary to restart the tactic interpreter after output is read. The sense of the rule infix used with output (normal or reverse) has no effect on its function.
The theorem INPUT causes the list of current hypotheses to be displayed (see next section) along with the current subterm (this is all the information relevant to the effect of the input). The user is then prompted to input a theorem to be applied to the current subterm. It is applied using the rule infix used with INPUT