-The basic tactic merely performs an iterated use of the Apply tactic
-(with no Intro). The research tree may be pruned according to two
-main parameters: the {\em depth} (whit the obvious meaning), and the
-{\em width} that is the maximum number of (new) open goals allowed at
-any instant. Matita has only one notion of metavariable, corresponding
-to the so called existential variables of Coq; so, Matita's Auto tactic
-should be compared with Coq's EAuto.
+The basic tactic merely iterates the use of the \TAC{apply} tactic
+(with no \TAC{intro}). The search tree may be pruned according to 2
+main parameters: the \emph{depth} (whit the obvious meaning), and the
+\emph{width} that is the maximum number of (new) open goals allowed at
+any instant. \MATITA{} has only one notion of metavariable, corresponding
+to the so called existential variables of Coq; so, \MATITA's \TAC{auto}
+tactic should be compared with \COQ's \TAC{EAuto} tactic.