[isabelle-dev] adhoc overloading

[Christian Sternagel]

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).

cheers

chris

-------------- next part --------------
A non-text attachment was scrubbed...
Name: ao.patch
Type: text/x-patch
Size: 6281 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130802/50924c97/attachment-0002.bin>