*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Monad_Syntax latex symbols*From*: Mathieu Giorgino <mathieu.giorgino at irit.fr>*Date*: Tue, 26 Apr 2011 15:26:07 +0200*In-reply-to*: <4DB67689.4000601@in.tum.de>*Organization*: IRIT*References*: <201104221937.04072.mathieu.giorgino@irit.fr> <4DB67689.4000601@in.tum.de>*User-agent*: KMail/1.13.6 (Linux/2.6.38-ARCH; KDE/4.6.2; x86_64; ; )

Le mardi 26 avril 2011 09:38:49, Alexander Krauss a écrit : > Hi Matthieu, > > > While compiling generated documents from theories, it seems some symbols > > of Monad_Syntax are missing. Should they be defined in isabellesym.sty ? > > As a user, you are free to define your own latex renderings of these > symbols... But we should probably add a sensible default... Ok, I had just thought it was an omission. By the way, I discovered the "do_notation" mode allowing to display monadic terms with the do-notation in antiquotations as well as in "term", "thm" (and perhaps others?): ---------- thm (do_notation) Ref.change_def text {* @{thm [mode=do_notation] Ref.change_def} *} ---------- Could this mode be set in a global way to be used by default in antiquotations? and also in proofs? Mathieu

**Follow-Ups**:**Re: [isabelle] Monad_Syntax latex symbols***From:*Makarius

**References**:**[isabelle] Monad_Syntax latex symbols***From:*Mathieu Giorgino

**Re: [isabelle] Monad_Syntax latex symbols***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Emacs/Isabelle crash
- Next by Date: Re: [isabelle] Monad_Syntax latex symbols
- Previous by Thread: Re: [isabelle] Monad_Syntax latex symbols
- Next by Thread: Re: [isabelle] Monad_Syntax latex symbols
- Cl-isabelle-users April 2011 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