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,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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