Built-in tactics:

BIND:

built-in tactic which converts the current subterm to a function of its term parameter, if this is permitted by stratification constraints. The BIND tactic now works sensibly when the parameter is a pair or more complex tuple.

EVAL:

built in tactic which reverses the effect of either BIND or UNEVAL; if applied to a term with a function (braket term) applied to an argument, it carries out the evaluation of the function at that argument.

INPUT:

built-in tactic which displays the local term and hypotheses and allows the user to enter a theorem to be applied at that point. The script command will read input intended for the INPUT command; in such input, comments are started by { and ended by } or the end of the line. } can be used to put more than one input theorem on a line. At the top level, the latest version of the prover causes a pause after the INPUT prompt, at which one can issue secure commands, including inputri to set the theorem to rewrite with. In scripts, the behavior of the prover has not changed: it reads theorems to be entered as lines of input from the script. The guimode(); command (which is deprecated) will restore the old behavior of INPUT at top level (if GUI mode is turned off).

FLIP:

built in tactic taking one argument (a theorem); the theorem parameter is applied if the selected subterm is an infix term with its two immediate subterms ``out of order''. Used for sorting (the parameter should be a commutative law, but this is not enforced).

OUTPUT:

built-in tactic which causes the prover to display its term parameter.

UNEVAL:

built-in tactic which converts the selected subterm to an application subterm in which the function is the term parameter, if this is possible. Upgrades in higher-order matching have considerably increased the scope of application of this tactic.

BINDM, EVALM, UNEVALM:

As BIND, EVAL, UNEVAL These built-in tactics handle abstraction and reduction for a more liberal kind of abstraction used to improve fluent treatment of first-order logic. These will be less important to typical users than the forms without the M.

SHELL (obsolete):

built-in tactic designed for use at the INPUT prompt. This tactic invokes the noml shell, so that the user can issue prover commands (e.g. display or search for theorems) from the INPUT environment. Recall that quit(); will terminate the noml shell. If the environment (the term being manipulated) is changed by the commands issued at the noml prompt, the prover will crash out in a manner similar to that which occurs with STOPINPUT. Do not attempt to carry out proofs in the shell invoked by this command! The SHELL tactic is now deprecated, since any top level invocation of INPUT now permits one to issue secure commands at the INPUT prompt. (Latest word is that it is completely obsolete).

STOPINPUT:

built-in tactic designed for use at the INPUT prompt: the effect is to convert the current term to an error term, causing the current execution to crash, returning to the first stage which invoked INPUT and issuing an error message. One can then edit and reissue the most recent block of theorems to be read at the INPUT prompt. STOPINPUT remains usable with the GUI modifications.

|-|:

operator which enables application of local hypotheses. 0|-|n applies the nth local hypothesis as a rewrite rule. 1|-|n reduces the selected subterm if it is a case expression with hypothesis identical to the nth local hypothesis. The converse of 1|-|n builds a new case expression with the nth local hypothesis (creating a new variable); the converse of 2|-|n is the same as the converse of 1|-|n, except that it takes a parameter which is used instead of the new variable.

UP:

a new (very experimental) built-in tactic. An execution of UP@?thm will cause ?thm to be executed on the parent term of the term to which it is applied, unless the parent term is itself an embedded theorem application. When two instances compete to be applied, the one on the right wins.

SCOUT, SCIN, SCINR, SCINL:

These built-in theorems allow application of the scin/scout witness theorem of the top-level operator or function of a target term, if there is one. These tactics add type labels when applied in the direct sense and eliminate them when applied in the converse sense, independently of the sense of the actual witness theorem.

=>> <<=:

``alternative rule infixes'': the effect of application of thm1 =>> thm2 is to apply thm1 (or its converse if the converse rule infix is used for the application) and apply thm2 (or its converse if <<= is used instead of =>>) just in case the application of thm1 fails. Failure of built-in tactics is defined as failure to change the selected term (this is not an optimal solution in theory, but seems to work in practice).

*> <*:

``guarded rule infixes'': just as the previous two infixes, except that thm2 is applied (in the appropriate sense) just in case the application of thm1 succeeds.

=:

When used as a built-in tactic, the tactic interpreter will search for a theorem or converse theorem justifying the equation used as an embedded theorem and apply it.

!@ !$:

``autoformat'' prefixes. Applying !@ (resp. !$) to a theorem produces a parameterized theorem taking a parameter list filling the new variables introduced by the theorem (resp. the converse of the theorem).

#!:

This unary operator on tactics was introduced to increase efficiency of execution of definitions of recursive functions. The first time an embedded theorem to which #! is applied is applied to a target, the result of this application is recorded; when it is applied subsequently, the result to be obtained is looked up in a table. This can save execution time. The argument of #! can be a tactic with arguments. Further, entries in the table can be applied in the converse sense as well, which can produce curious effects!