Re: [isabelle] declaration attribute



On Tue, 20 Mar 2012, Ondřej Kunčar wrote:

I want to define a declaration attribute which works with the given theorem. I've already implemented this operation in the function foo :: thm -> local_theory -> local_theory. Now I want to define a attribute by the function Thm.declaration_attribute :: (thm -> Context.generic -> Context.generic) -> Thm.attribute.

What is your local_theory -> local_theory operation actually doing? If it does genuine specifications (like Local_Theory.define) than it cannot be a "declaration" at the same time.

A declaration is some kind of generic data update on a generic context. It needs to work in many situations, like the original local_theory context of the user, its background theory, any other application context after interpretation, and more.

This is also the reason, why such declarations need to fail gracefully, if they don't like their argument, and not prevent other declarations from succeeding that happened to be pulled-in by the same locale interpretation, for example.


	Makarius


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