[isabelle] Relation of function absent from Main



Hello,

I have been using the following function extensively:

definition rel_of :: "('a ⇒ 'a) ⇒ 'a rel" where "rel_of f = {(x,y) . f x = y}"

This seems to be absent from the Isabelle libraries, despite being obvious. Am I missing something, or is it perhaps a bad idea to convert between functions and relations?

Best regards,
Christian Pardillo Laursen


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