Hi Stefan, > They were removed from the pred_set_conv database a while ago by Florian > > http://isabelle.in.tum.de/repos/isabelle/rev/7f9e05b3d0fb > > because they were considered "potentially dangerous", but now that sets > and predicates can be distinguished again, this rule (and the dual rule > sup_Un_eq) could be added again?
yes, they can. The where »dangerous« as long as both sets and preds
*and* union/inter and sup/inf were identified. With sets being
different from preds, they can be reactivated.
This is indeed one thing which has slipped out of my memory.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
