[isabelle-dev] adhoc overloading

[Makarius]

On Fri, 2 Aug 2013, Christian Sternagel wrote:

> On 08/02/2013 12:04 AM, Makarius wrote:
>> On Wed, 17 Jul 2013, Christian Sternagel wrote:
>> 
>>> in case anybody finds localized ad-hoc overloading useful.
>> 
>> Quite often it is just a matter to tell users about the existence of
>> such useful tools.
>> 
>> Do you feel like making an example theory, e.g.
>> src/HOL/ex/Adhoc_Overloading_Examples.thy or a short entry for the
>> isar-ref manual?  E.g. somewhere here
>> http://isabelle.in.tum.de/repos/isabelle/annotate/122416054a9c/src/Doc/IsarRef/HOL_Specific.thy
>
> I gave both a try. Please find the resulting changesets (via "hg export") 
> attached (I also squeezed in some unrelated changes: spell-checking, tuning 
> of error messages. I hope that is okay).

The tuning etc. is fine (it looks like done with care).

What is missing in the commit is your new file 
src/HOL/ex/Adhoc_Overloading_Examples.thy


 	Makarius