Re: [isabelle] Newlines in antiquotation output

Hi Chris,

On Sat, 23.06.2012 04:25, Christian Sternagel wrote:
> you can read the section on Inner syntax of the Isabelle Reference 
> Manual (isabelle doc isar-ref). There it is described how to use mixfix 
> annotations (which can be installed just for certain output modes, e.g., 
> like (latex)) to configure pretty printing. Something very similar to 
> your example is available as part of Monad_Syntax.thy from 
> Isabelle/HOL's library:

Thank you, that seems work nicely. I ended up defining the notations I
wanted myself instead of using do notation though, but the Monad_Syntax
theory is a nice example of how to do that.


Attachment: pgpJTAQENFYEW.pgp
Description: PGP signature

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