Re: [isabelle] adhoc_overloading Monad_Syntax.bind



Cool, that helps!

Tobias

On 12/02/2016 11:50, Makarius wrote:
On Fri, 12 Feb 2016, Tobias Nipkow wrote:

Thank you for the link. It mentions [[show_variants]] which would solve some
of my problems. Can that be used locally in a term antiquotation? This does
not work @{term [show_variants] ...}

Try this:

setup â
   Thy_Output.add_option @{binding show_variants}
     (Config.put Adhoc_Overloading.show_variants o Thy_Output.boolean)â


     Makarius

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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