*To*: Gergely Buday <gbuday at gmail.com>*Subject*: Re: [isabelle] using arrows in text{* *}*From*: Makarius <makarius at sketis.net>*Date*: Wed, 2 Jul 2014 20:14:48 +0200 (CEST)*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <CA+3iOz=e8Q0LeYt03XMYFio63R+L8+DpSa31Qq2q0fV6Tfkh_A@mail.gmail.com>*References*: <CA+3iOz=e8Q0LeYt03XMYFio63R+L8+DpSa31Qq2q0fV6Tfkh_A@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 proofdocument?

Makarius

**References**:**[isabelle] using arrows in text{* *}***From:*Gergely Buday

- Previous by Date: Re: [isabelle] using arrows in text{* *}
- Next by Date: Re: [isabelle] Surpress warning-squiggly lines in JEdit
- Previous by Thread: Re: [isabelle] using arrows in text{* *}
- Next by Thread: [isabelle] New in the AFP: Pop-Refinement
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list