**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*n*th local hypothesis as a rewrite rule.`1|-|n`reduces the selected subterm if it is a case expression with hypothesis identical to the*n*th local hypothesis. The converse of`1|-|n`builds a new case expression with the*n*th 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!