Re: [isabelle] declaration attribute

On 03/20/2012 08:42 PM, 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. Although I invested a non-trivial time to try to figure out how to go from Context.generic to local_theory and back, I wasn't successful. Can anybody please help me and tell me how to implement the "boilerplate" function bar in "Thm.declaration_attribute bar" such that bar is implemented in terms of the function foo?



The function Context.mapping is probably what you want.


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