[isabelle-dev] "interpret ... for a" leaks a

[Florian Haftmann]

Hi Lars,

> in 40fe6b80b481, I stumbled upon the following behaviour. Consider
> the following example:
> 
>   locale Foo = fixes a :: 'a
> 
>   notepad begin
>     interpret Foo b for b .
>     term b
>   end
> 
> jEdit tells me about b in the term command:
> 
>   term
>   fixed "b"
>   skolem variable
>   :: 'b
> 
> So the b from the "for b" is leaked into the surrounding context. As all
> the lemmas about b where generalized, I would have expected that
> b does not become fixed in the surrounding context.

I guess the for-parameters are not dealt as expected by interpret.
Maybe this is a co-phenomenon of the following warning from isar-ref:

> interpret expr where eqns interprets expr in the proof context and is
> otherwise similar to interpretation in local theories. Note that rewrite
> rules given to interpret after the where keyword should be explicitly
> universally quantified.

Cheers,
	Florian Haftmann

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130529/227abe01/attachment.sig>