Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:55):

From: Gergely Buday <gbuday@gmail.com>
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?

view this post on Zulip Email Gateway (Aug 19 2022 at 14:56):

From: Christian Sternagel <c.sternagel@gmail.com>
Without seeing your actual theory content it's hard to say what went
wrong. -cheers chris

view this post on Zulip Email Gateway (Aug 19 2022 at 14:57):

From: Makarius <makarius@sketis.net>
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.

Makarius

Last updated: Apr 26 2024 at 20:16 UTC