Re: [isabelle] using arrows in text{* *}

On Wed, 2 Jul 2014, Gergely Buday wrote:

I tried to use \<longleftrightarrow> and later its LaTeX equivalent in
a text{* *} block and got

Is this regular behaviour? How can I put such arrows into the proof document?

You need to make such Isabelle symbols formal within the quoted informal LaTeX, e.g. via the antiquotation @{text}.

I recommend to look at existing examples how Isabelle documents are generally done. AFP has tons of material.


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