[isabelle-dev] adhoc overloading

[Makarius]

On Wed, 17 Jul 2013, Christian Sternagel wrote:

> Here are two follow-up patches (this time generated by "hg export") that 
> improve error messages for multiple instances (actually showing the 
> existing instances to the user).

I have imported them as 72cda5eb5a39 and 1e13b2515e2b.

BTW, the log message format allows several items, but these should be put 
on a separate line each (with terminator as you've had already).  This 
format is meant for speed-reading of changelogs, e.g. see this view:

   http://isabelle.in.tum.de/repos/isabelle/log/52688

(It also shows that many people have already forgotten that.)

In the old times log entries were extremely short.  In recent years the 
art of squezing additional reasoning and explanations into each item-line 
has further developed, but too much blah blah is not good.


Anyway, I still need to read through your present implementation to give a 
few further hints, e.g. concerning the question about type inference in a 
local context that emerged recently.  It should all work, if the "proper 
context" is used.


 	Makarius