[isabelle-dev] Attributes and local theories
schropp at in.tum.de
Mon Nov 14 23:29:09 CET 2011
On 11/14/2011 09:49 PM, Andreas Schropp wrote:
> the idea of a non-pervasive declaration (with the new semantics) is
> that the resulting
> context modifications are registered for the target (if necessary,
> i.e. in the case of locales)
> and they are also applied to the auxilliary context (which is not
> shared between applications
> of different morphisms and goes out of scope with the target)?
> I guess this is what I need then.
> BTW: this cannot easily be achieved with the old semantics
> (which don't modify the aux ctxt), right?
fun add_non_pervasive_declaration decl lthy =
|> Local_Theory.declaration false decl
|> Context.proof_map (Morphism.form decl)
should do the job based on Isabelle2011-1's Local_Theory.declaration?
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev