The semantic interpretation of bracket terms as functions is enforced
by the three built-in tactics `BIND`, `EVAL` and `UNEVAL`.

`BIND` takes a parameter: when `BIND @ T` is applied to a
term `U` at level *l*, the effect is to translate `U` to level
*l*+1, replace all occurrences of the result of translating `T` to
level *l*+1 in the translation of `U` by occurrences of `?[l+1]` (we hope that this is a pardonable abuse of notation),
enclose the result in brackets and apply it (using `@` to
represent function application) to `T`; this process only succeeds
if the bracket term obtained is stratified (otherwise `U` is
unchanged). In terms of -notation, the result can be
described as
.

`EVAL` takes no parameter; when `EVAL` is applied to a term of
the form `[T] @ U` at level *l*, the effect is to translate `U` to
level *l*+1, replace `?[l+1]` with the translated form of `U`
in `T`, and translate this modified form of `T` from level
`?[l+1]` to level `l`; this modified form of `T` is the
result. Mathematically, this is simply -reduction, and it
always succeeds.

`UNEVAL` is a little more esoteric, and it took some experience to
realize that it was needed. When `UNEVAL @ [T]` is applied to
`U`, the result is a term of the form `[T] @ X` precisely if
there is such a term which would reduce to `U` on application of
`EVAL`. The effect of `UNEVAL` is to rewrite an expression as
a value of the function given as its parameter if this is possible.

The project of providing built-in support to synthetic abstraction and reduction algorithms found in the original prover EFTTP (as discussed in our reference [14]) and still supported by little-used features of Mark2 has been abandoned. Synthetic abstraction and reduction algorithms are straightforward to implement in the tactic language of Mark2 or Watson. We are still carrying out investigations in this area using the Watson tactic language as a tool. But we no longer see it as reasonable to support this in the prover's built-in logic.