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
------------------------------------------------------------------------------
Meet PCI DSS 3.0 Compliance Requirements with EventLog Analyzer
Achieve PCI DSS 3.0 Compliant Status with Out-of-the-box PCI DSS Reports
Are you Audit-Ready for PCI DSS 3.0 Compliance? Download White paper
Comply to PCI DSS 3.0 Requirement 10 and 11.5 with EventLog Analyzer
http://pubads.g.doubleclick.net/gampad/clk?id=154622311&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
