Re: [isabelle] Monad_Syntax latex symbols

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?


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