Re: [Hol-info] munger on strings containing backslash

[Michael N. <Mic...@ni...>]

I think the commits you pushed to the repository (a83e2652 and 0802f86b) are fine fixes for this.

Michael

On 29 Sep 2014, at 2:13 am, Ramana Kumar <Ram...@cl...> wrote:

> 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
> hol...@li...
> https://lists.sourceforge.net/lists/listinfo/hol-info


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.