Re: [isabelle] Dependencies on constants
Am 23.06.2010 um 10:13 schrieb Rafal Kolanski:
> That's amazing. I think it may be exactly what I've been looking for! I really should have asked the list sooner rather than banging my head against the wall for hours.
>> The advantage of Spec_Rules is that it returns simplification rules
>> for recursive functions rather than the raw definition, intro rules
>> for (co)inductive predicates, etc.
> Is there any disadvantage you know of? For example, non-bizarre ways of introducing constants that don't show up in this list?
I don't know for sure. I haven't ported my "Defs"-based code to "Spec_Rules" yet. Lukas uses "Spec_Rules" for the predicate compiler; maybe he has some insights to share.
I would definitely suggest you try with "Spec_Rules" first and use "Defs" as a fallback.
This archive was generated by a fusion of
Pipermail (Mailman edition) and