[isabelle-dev] adhoc overloading

Makarius makarius at sketis.net
Thu Aug 1 17:04:39 CEST 2013

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 

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.


More information about the isabelle-dev mailing list