+The following simple example shows three tacticals in action
+\begin{grafite}
+theorem trivial:
+ \forall A,B:Prop.
+ A = B \to ((A \to B) \land (B \to A)).
+ intros (A B H).
+ split; intro;
+ [ rewrite < H. assumption.
+ | rewrite > H. assumption.
+ ]
+qed.
+\end{grafite}
+
+The first is ``\texttt{;}'' that combines the tactic \texttt{split}
+with \texttt{intro}, applying the latter to each goal opened by the
+former. Then we have ``\texttt{[}'' that branches on the goals (here
+we have two goals, the two sides of the logic and).
+The first goal $B$ (with $A$ in the context)
+is proved by the first sequence of tactics
+\texttt{rewrite} and \texttt{assumption}. Then we move to the second
+goal with the separator ``\texttt{|}''. The last tactical we see here
+is ``\texttt{.}'' that is a sequential composition that selects the
+first goal opened for the following tactic (instead of applying it to
+them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
+not considered a tactical, but a sentence terminator (i.e. the
+delimiter of commands the proof assistant executes).
+
+Giving serious examples here is rather difficult, since they are hard
+to read without the interactive tool. To help the reader in
+understanding the following considerations we just give few common
+usage examples without a proof context.
+
+\begin{grafite}
+ elim z; try assumption; [ ... | ... ].
+ elim z; first [ assumption | reflexivity | id ].
+\end{grafite}
+
+The first example goes by induction on a term \texttt{z} and applies
+the tactic \texttt{assumption} to each opened goal eventually recovering if
+\texttt{assumption} fails. Here we are asking the system to close all
+trivial cases and then we branch on the remaining with ``\texttt{[}''.
+The second example goes again by induction on \texttt{z} and tries to
+close each opened goal first with \texttt{assumption}, if it fails it
+tries \texttt{reflexivity} and finally \texttt{id}
+that is the tactic that leaves the goal untouched without failing.
+
+Note that in the common implementation of tacticals both lines are
+compositions of tacticals and in particular they are a single
+statement (i.e. derived from the same non terminal entry of the
+grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
+this is not true, since each atomic tactic or punctuation is considered
+a single statement.
+
+\subsubsection{Common issues of tactic(als)-based proof languages}
+We will examine the two main problems of tactic(als)-based proof script:
+maintainability and readability.
+
+Huge libraries of formal mathematics have been developed, and backward
+compatibility is a really time consuming task. \\
+A real-life example in the history of \MATITA{} was the reordering of
+goals opened by a tactic application. We noticed that some tactics
+were not opening goals in the expected order. In particular the
+\texttt{elim} tactic on a term of an inductive type with constructors
+$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
+\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
+but some theorems about integers were there. The inductive type of
+$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
+induction proofs on this type where written without tacticals and,
+obviously, considering the three induction cases in the wrong order.
+Fixing the behavior of the tactic broke the library and two days of
+work were needed to make it compile again. The whole time was spent in
+finding the list of tactics used to prove the third induction case and
+swap it with the list of tactics used to prove the second case. If
+the proofs was structured with the branch tactical this task could
+have been done automatically.
+
+From this experience we learned that the use of tacticals for
+structuring proofs gives some help but may have some drawbacks in
+proof script readability. We must highlight that proof scripts
+readability is poor by itself, but in conjunction with tacticals it
+can be nearly impossible. The main cause is the fact that in proof
+scripts there is no trace of what you are working on. It is not rare
+for two different theorems to have the same proof script (while the
+proof is completely different).\\
+Bad readability is not a big deal for the user while he is
+constructing the proof, but is considerably a problem when he tries to
+reread what he did or when he shows his work to someone else. The
+workaround commonly used to read a script is to execute it again
+step-by-step, so that you can see the proof goal changing and you can
+follow the proof steps. This works fine until you reach a tactical. A
+compound statement, made by some basic tactics glued with tacticals,
+is executed in a single step, while it obviously performs lot of proof
+steps. In the fist example of the previous section the whole branch
+over the two goals (respectively the left and right part of the logic
+and) result in a single step of execution. The workaround doesn't work
+anymore unless you de-structure on the fly the proof, putting some
+``\texttt{.}'' where you want the system to stop.\\
+
+Now we can understand the tradeoff between script readability and
+proof structuring with tacticals. Using tacticals helps in maintaining
+scripts, but makes it really hard to read them again, cause of the way
+they are executed.
+
+\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}