[isabelle-dev] Interpretation in arbitrary targets.

[Makarius]

On Tue, 26 Mar 2013, Florian Haftmann wrote:

> Recently the local theory concept has been enriched with free-floating 
> contexts
>
> 	context
> 	  fixes … assumes …
> 	begin
>
>  	…
>
> 	end
>
> Now what would
>
> 	context
> 	  …
> 	begin
>
>  	…
>
> 	interpretation
>
> 	…
>
> 	end
>
> be?  Currently, there is check that »interpretation« may only be issued
> at the bottom level of the local theory stack, outside any free-floating
> context.  Although I have no constructive proof at hand yet, I believe
> that by lifting the check appropriately we get b) for free: similar to
> »interpret«, this would only yield facts inside the context (whose
> bindings disappear after »end«) without any additional dependencies or
> registrations.

(I still need to study the material on this thread carefully.  Right now 
just a quick interjection.)

Does that mean that 'interpretation' within unnamed 'context begin ... 
end' is without permanent subscription, but "in" a named target context or 
the global theory it is still with subscription as before?


 	Makarius