+\MATITA{} uses a language of tactics and tacticals, but tries to avoid
+this tradeoff, alluring the user to write structured proof without
+making it impossible to read them again.
+
+\subsubsection{The \MATITA{} approach: Tinycals}
+
+\begin{table}
+ \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
+\hrule
+\[
+\begin{array}{@{}rcll@{}}
+ \NT{punctuation} &
+ ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
+ \NT{block\_kind} &
+ ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
+ \NT{block\_delimiter} &
+ ::= & \verb+begin+ ~|~ \verb+end+ & \\
+ \NT{tactical} &
+ ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
+While one would expect to find structured constructs like
+$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
+This is essential for base idea behind matita tacticals: step-by-step execution.
+
+The low-level tacticals implementation of \MATITA{} allows a step-by-step
+execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
+not executed as an atomic operation. This has two major benefits for the user,
+even being a so simple idea:
+\begin{description}
+\item[Proof structuring]
+ is much easier. Consider for example a proof by induction, and imagine you
+ are using classical tacticals in one of the state of the
+ art graphical interfaces for proof assistant like Proof General or Coq Ide.
+ After applying the induction principle you have to choose: structure
+ the proof or not. If you decide for the former you have to branch with
+ ``\texttt{[}'' and write tactics for all the cases separated by
+ ``\texttt{|}'' and then close the tactical with ``\texttt{]}''.
+ You can replace most of the cases by the identity tactic just to
+ concentrate only on the first goal, but you will have to go one step back and
+ one further every time you add something inside the tactical. Again this is
+ caused by the one step execution of tacticals and by the fact that to modify
+ the already executed script you have to undo one step.
+ And if you are board of doing so, you will finish in giving up structuring
+ the proof and write a plain list of tactics.\\
+ With step-by-step tacticals you can apply the induction principle, and just
+ open the branching tactical ``\texttt{[}''. Then you can interact with the
+ system reaching a proof of the first case, without having to specify any
+ tactic for the other goals. When you have proved all the induction cases, you
+ close the branching tactical with ``\texttt{]}'' and you are done with a
+ structured proof. \\
+ While \MATITA{} tacticals help in structuring proofs they allow you to
+ choose the amount of structure you want. There are no constraints imposed by
+ the system, and if the user wants he can even write completely plain proofs.
+
+\item[Rereading]
+ is possible. Going on step by step shows exactly what is going on. Consider
+ again a proof by induction, that starts applying the induction principle and
+ suddenly branches with a ``\texttt{[}''. This clearly separates all the
+ induction cases, but if the square brackets content is executed in one single
+ step you completely loose the possibility of rereading it and you have to
+ temporary remove the branching tactical to execute in a satisfying way the
+ branches. Again, executing step-by-step is the way you would like to review
+ the demonstration. Remember that understanding the proof from the script is
+ not easy, and only the execution of tactics (and the resulting transformed
+ goal) gives you the feeling of what is going on.
+\end{description}
+
+\section{The Matita library}