Re: [isabelle] Dependencies on constants



Hi Rafal,

>> he 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.

it depends what you actually aiming it.  The Defs module represents the
proof theoretic aspect of definitions, i.e. constants which depend on
other constants.  The Spec_Rules represent more the end-user view of
"initial specification".

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.