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, this looks like a bug. The culprit seems to be function mk_to_pred_inst in inductive_set.ML, which does not handle variables of type "... => T set" properly. A similar problem might also occur with to_set. I'll try to fix this before the next release. Greetings, Stefan _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
