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.