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? :)
A minimal (and therefore nonsensical) example:
inductive_set foo :: "('a * 'a) set"
where "(a, b) : foo"
inductive_set bar :: "('a * 'a) set"
where "foop a b ==> (a, b) : bar"
Here I obtain bar.intros
"(?a, ?b) : foo ==> (?a, ?b) : bar
but I would rather like to have
"foop ?a ?b ==> (?a, ?b) : bar"
(that is, what I have written in the definition).
This archive was generated by a fusion of
Pipermail (Mailman edition) and