florian.haftmann at informatik.tu-muenchen.de
Fri Jan 13 21:09:06 CET 2012
> They were removed from the pred_set_conv database a while ago by Florian
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev