[isabelle-dev] Additional type variable(s) in specification
makarius at sketis.net
Thu Dec 2 17:42:23 CET 2010
On Thu, 2 Dec 2010, Tobias Nipkow wrote:
> Florian explained to me that for the function package this new behaviour
> is an improvement, but that does not mean that unsuspecting users should
> be subjected to it.
Maybe Florian (and Alex) can post again the concrete examples they were
mentioning to me 1 or 2 years ago.
As usual with the locale and locale theory specification business, the
situation is a bit more complex than most people think. The version of
09e238561460 is one more step towards *less* surprise in this notoriously
difficult issue of hidden polymorphism. The same technique of itself
abstractions is used in several other parts of the system, too.
Right now there is already a clear warning -- which Proof General happens
to show in a hardly visible way, but that is just one of many problems of
Proof General. In Isabelle/jEdit the warning is hard to miss. I will
check again about the other related messages to increase the pontential
More information about the isabelle-dev