[Hol-info] munger on strings containing backslash

[Ramana K. <Ram...@cl...>]

Hi all,

I'm having trouble figuring out how to add theorems that include string
literals into my LaTeX document, when the strings might contain a
backslash. The munger produces something like:
  \HOLStringLit{\\/}
which, when inside a math environment, confuses LaTeX a lot.

Does anyone have an idea for a workaround? Is there some way within HOL to
tweak the printing of string literals so I could say temporarily replace
the special characters with some other placeholder that can then be
rewritten back to something appropriate within LaTeX?

Cheers,
Ramana