[isabelle] declaration attribute



Hi!
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?

Thanks.

Ondrej





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