Re: [isabelle] How to use latex commands inside proof?

Hi Holden,

if you use the delimiters {* and *} instead of " " for the LaTeX text, then antiquotations and escaping work as expected. In Isabelle2014, you can alternatively use the cartouche \<open> and \<close>. Instead of an inline comment introduced by --, you can also use regular text blocks with txt as in

  txt {* $a \in A$ *}


On 28/08/14 14:41, Holden Lee wrote:
I'd like to put in some comments like so:

proof -
-- "some typeset math here like $a \in A$"

but it seems like \ can't be used, and \\ doesn't escape it. What's the
correct way?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.