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?
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
