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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and