<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">

<html>

<head>

  <meta content="text/html; charset=ISO-8859-1"

 http-equiv="Content-Type">

</head>

<body text="#000000" bgcolor="#ffffff">

<tt>On 11/14/2011 09:49 PM, Andreas Schropp wrote:<br>

</tt>

<blockquote cite="mid:4EC17EDD.2090306@in.tum.de" type="cite"><tt>  the

idea of a non-pervasive declaration (with the new semantics) is that

the resulting

  <br>

context modifications are registered for the target (if necessary, i.e.

in the case of locales)

  <br>

and they are also applied to the auxilliary context (which is not

shared between applications

  <br>

of different morphisms and goes out of scope with the target)?

  <br>

  <br>

I guess this is what I need then.

  <br>

BTW: this cannot easily be achieved with the old semantics

  <br>

(which don't modify the aux ctxt), right?

  <br>

  <br>

  </tt>

</blockquote>

<tt><br>

But <br>

</tt>

<blockquote><tt>fun add_non_pervasive_declaration decl lthy =<br>

  lthy<br>

  |> Local_Theory.declaration false decl<br>

  |> Context.proof_map (Morphism.form decl)</tt><br>

</blockquote>

should do the job based on Isabelle2011-1's Local_Theory.declaration?<br>

</body>

</html>