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.

Jasmin






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