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

proof
  ...
  txt {* $a \in A$ *}
  ..
end

Best,
Andreas

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?

-Holden





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