- apply type constructors or try to automatically conclude equality goals)
- only the tactic name is represented in the hint. For tactics that need terms
- as arguments (for example the \emph{Apply} tactic) the hint includes a
- textual representation of them, using the same representation used by the
- interactive proof assistant when querying user for terms. In order to be
- trasmitted between \wss, hints are serialized in XML.
-
- Actually it is also possible for a tutor to return more hints at once,
+ apply type constructors or decision procedures)
+ only the tactic name is represented in the hint. For tactics that need
+ terms as arguments (for example the \texttt{Apply} tactic that apply a
+ given lemma) the hint includes a textual representation of them, using the
+ same representation used by the interactive proof assistant when querying
+ user for terms. In order to be trasmitted between \wss{}, hints are
+ serialized in XML.
+
+ It is also possible for a tutor to return more hints at once,