On Thu, Dec 2, 2010 at 8:42 AM, Makarius <[email protected]> wrote: > 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 further.
Making the warning message more visible is only a partial solution. The wording of the warning itself is also a problem: "Additional type variable(s) in specification" Users who encounter this warning because of a mistake in a definition are unlikely to know what it means (unless they have read about it on the mailing list). More importantly, the warning message doesn't give any hints about how to fix the mistake. - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
