Add additional comment on optional syntax

Manual/Description/definitions.stex

@@ -2036,10 +2036,12 @@ one writes
 \end{verbatim}
 where, as with other special syntaxes, the keywords (\ml{Inductive} and \ml{End}) have to be in the leftmost column of the source file.
 Additionally, users can automatically export each rule as a theorem by assigning a name using the square-bracket syntax.
-The appropriate format is \holtxt{[\(\sim\)Name:]}, where \holtxt{Name} acts as the placeholder for the rule name, see the following example:
+The appropriate format is \holtxt{[\textasciitilde Name:]}, where \holtxt{Name} acts as the placeholder for the rule name.
+Inside the square brackets, the tilde (\textasciitilde) is optional; if included, it prefixes the exported rule name with \ml{<stem>\_}.
+For instance, the following example will export rules as \ml{rule1} and \ml{foo\_rule2}.
 \begin{verbatim}
    Inductive foo:
-   [~rule1:]
+   [rule1:]
      ...
    [~rule2:]
      ...