Re: [isabelle] adhoc_overloading Monad_Syntax.bind



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


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