[isabelle-dev] adhoc overloading

[Christian Sternagel]

Dear Makarius,

actually even more is missing, since I was not able to properly use "hg 
export" (I am used to "hg bundle" which "exports" *all* changesets that 
are only local, whereas for "hg export" I have to give all revisions 
that should be exported explicitly). Sorry for that. Please find 
attached a file containing all my changes.

cheers

chris

On 08/06/2013 03:34 AM, Makarius wrote:
> 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

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