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 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 specific versions. Unfortunately, the Relation theory is currently a bit of a mess. Larger blocks of conversion lemmas are commented out for no good reason, which means that they are not tested by our nightly builds, and for some of them it still remains to be examined whether they can be added to the database of predicate/set conversion rules by default without breaking any of the examples in the AFP. What is the strategy for cleaning up this theory? Greetings, Stefan _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev