We discuss some miscellaneous built-in tactics.
INPUT and OUTPUT allow interaction between a tactic and the user. The INPUT command displays the local hypotheses and the selected subterm; the prover then waits for the user to enter a theorem or tactic, which will then be applied. If the user hits return, the prover will simply continue. The OUTPUT command simply displays its term parameter. The INPUT command has been used in the development of a goal-driven natural deduction prover as a family of Watson tactics.
The FLIP command takes a parameter, intended to be the name of a theorem (in fact, intended to be a ``commutative law'', though the prover does not enforce this). If FLIP @ ?thm is applied to an infix term the displayed forms of whose arguments are not in lexicographic order, the theorem ?thm is applied; otherwise nothing is done. The intention is to support the ability to define canonical forms for expressions built with commutative operators, by sorting terms.