Hi,
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.
-- Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
