[isabelle-dev] adhoc overloading
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
> 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