Manual/Description/misc.tex

1138 By default, the HOL pretty-printer is paranoid about token-merging, and will insert spaces between the tokens it emits to try to ensure that what is output can be read in again without error.
1146 (In interactive HOL, the token-merging analysis is controlled by a trace variable called \texttt{"pp\_avoids\_symbol\_merges"}.)
1319 \item[$s\mathtt{//}t$] (For use with \holtm{}, \holthm, and \holty) Causes \LaTeX{} string $s$ to be substituted for token $t$.
1323 The width of the \LaTeX{} string is taken to be the width of the original token $t$.
1412 token-to-\LaTeX{} replacements of what is pretty-printed.
1422 where \texttt{tok} is a \HOL{} token, \texttt{width} is a number
1446 By overriding the special token \texttt{\$Turnstile\$}, one can control the printing of the turnstile produced by \holthm{}.
1463 \paragraph{Preventing Merge Analysis}  As mentioned above in the description of the \texttt{merge} and \texttt{nomerge} options to the \holtm{} and \holthm{} commands, the munger can be configured to not do token-merging avoidance by passing the \texttt{--nomergeanalysis} option to the munger.
1681 token-to-\LaTeX{} replacements of what is pretty-printed.
1699 Though one might specify all one's desired token-replacements in an \texttt{overrides} file, there is also support for specifying token replacements in the theory where tokens are first ``defined''.
1703 A token's printing form is given in a script-file with the \ml{TeX\_notation} command (from the \ml{TexTokenMap} module).
1709 The \ml{hol} field specifies the string of the token as \HOL{} prints it.
1723 Finally, rather than mapping the token directly to the string \texttt{\bs{}forall} as one might expect, the mapping introduces another level of indirection by mapping to \texttt{\bs{}HOLTokenForall}.