## Interactive proofs and definitions

An interactive definition is started by giving a
definition command omitting
the definiens.
An interactive proof is started by using one of the
proof commands omitting
an explicit proof term.

An interactive proof or definition can and must be terminated by
a qed command when no more sequents are
left to prove. Between the command that starts the interactive session and
the qed command the user must provide a procedural proof script made
of tactics structured by means of
tacticals.

In the tradition of the LCF system, tacticals can be considered
higher order tactics. Their syntax is structured and they are executed
atomically. On the contrary, in Matita the syntax of several tacticals is
destructured into a sequence of tokens and tactics in such a way that is
is possible to stop execution after every single token or tactic.
The original semantics is preserved: the execution of the whole sequence
yields the result expected by the original LCF-like tactical.