Re: [isabelle] Monad_Syntax latex symbols

On Tue, 26 Apr 2011, Mathieu Giorgino wrote:

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.

Isabelle provides infinitely many symbols, but only a finite list of well-known ones are defined in the default LaTeX styles. This is done in a way that avoids conflicts of LaTeX packages, i.e. isabellesym.sty does not force any packages on the user.

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?

This is the normal Isabelle "print mode". You can modify it in some command line tools like "usedir" using option -m, for example. For document preparation there is a global default Thy_Output.modes, which can be set in ROOT.ML.


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