[isabelle-dev] adhoc overloading

Makarius makarius at sketis.net
Mon Aug 5 20:34:38 CEST 2013

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 


More information about the isabelle-dev mailing list