next up previous contents
Next: The Special Theorem ORDERED Up: The Tactic Language Previous: Arithmetic Operators

The Special Theorems INPUT and OUTPUT

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

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997