Matita HomeMatita HomeTable of Contents
+ 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.