Re: [isabelle] inductive_set

Hi Christian,

> apparently inductive_set does modify ALL occurrences of inductive
> predicates stemming from other inductive_set commands inside intro rules
> as if the attribute [to_set] was used. Is this wanted / necessary / on
> purpose? Can I prevent it? :)

according to the sources inductive_set seems indeed to behave like that.
 You may call this a bug or a feature.

The rules used for to_set / to_pred conversions are added using
attribute pred_set_conv.  Unfortunately, this only allows addition, not
removal, preventing an ad-hoc solution for your problem.  Maybe we have
to think about that.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.