[isabelle-dev] adhoc overloading

[Makarius]

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

Strictly speaking it is probably not HOL specific, but re-use of the Pure 
type language within the object-logic is somehow part of the specific 
Isabelle/HOL tradition.


 	Makarius