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.