[isabelle] adhoc_overloading Monad_Syntax.bind



I have problems combining adhoc_overloading Monad_Syntax.bind with abbreviations. In the context of HOL-Probability:

adhoc_overloading Monad_Syntax.bind bind_pmf

abbreviation "f x y == (bind_pmf x (return_pmf o Pair y))"
term "f a b"

The output of the "term" command is the ugly rhs of the abbreviation (with infix >>=). How can I phrase the abbreviation to make it work? Maybe with the help of some translation?

Thanks a lot for quick answers!
Tobias

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



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