Tobias On 19/02/2021 18:38, Christian Pardillo Laursen wrote:
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
Attachment:
smime.p7s
Description: S/MIME Cryptographic Signature