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



Without seeing your actual theory content it's hard to say what went wrong. -cheers chris

On 07/02/2014 05:30 PM, Gergely Buday wrote:
Hi,

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

*** Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
*** (hyperref)                removing `\OT1/cmtt/m/n/10.95' on input line 246.
***
***
*** Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
*** (hyperref)                removing `\ignorespaces' on input line 246.

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

- Gergely





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