Re: [isabelle-dev] Conversions between ('a * 'a) set and 'a = 'a = bool relations

Florian Haftmann wrote: * This is mainly a question to Stefan: there are some theorems commented out (e.g. »thm sym_INTER [to_pred]«) on which pred_set_conv chokes. I guess this is due to a higher-order situation, but I would be reassuring if you can confirm that. Hi Florian, I have fixed

Re: [isabelle-dev] Conversions between ('a * 'a) set and 'a = 'a = bool relations

Hi Stefan, I have fixed this bug now, see changeset b1d15637381a. Note that converting the above theorem (and the other theorems in Relation.thy marked with FIXME) to predicate notation requires the generalized versions of theorems INF_INT_eq2 and SUP_UN_eq2, which should replace the more