[isabelle-dev] Attributes and local theories

[Andreas Schropp]

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

But

    fun add_non_pervasive_declaration decl lthy =
       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...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20111114/d46ed5d6/attachment-0002.html>