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.