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

On Thu, 28 Aug 2014, Andreas Lochbihler wrote:

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

`Yes. Moreover, there is usually little need to produce actual LaTeX math
``in Isabelle documents. You can just use interpreted or uninterpreted
``antiquotations like this:
`
txt {* @{prop "a \<in> A"} *}
txt {* @{text "a \<in> A"} *}

`This has the advantage that the input and typeset output is uniform
``according to Isabelle standards, although the pseudo-math mode of
``isabelle.sty is a bit weaker than actual math mode.
`
Makarius

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