[isabelle] using arrows in text{* *}



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.