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:
>
> http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Monad_Syntax.html

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.

Regards,
Daniel

Attachment: pgpJTAQENFYEW.pgp
Description: PGP signature



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